Theorem excom 728

Description: Theorem 19.11 of [Margaris] p. 89.

Assertion

Ref	Expression
excom	⊢ (∃x∃yφ ↔ ∃y∃xφ)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		excomim 727	. 2 ⊢ (∃x∃yφ → ∃y∃xφ)
2		excomim 727	. 2 ⊢ (∃y∃xφ → ∃x∃yφ)
3	1, 2	impbi 139	1 ⊢ (∃x∃yφ ↔ ∃y∃xφ)

Syntax hints:   ↔ wb 127  ∃wex 678

This theorem is referenced by:  excom13 776  exrot3 777  ee4anv 982  2euex 1061  2exeu 1066  2eu1 1067  2eu4 1070  rexcom 1313  gencbvex 1372  dfiun2 2014  iunn0 2029  opabid 2099  dmuni 2538  dm0rn0 2549  dmco 2570  dmcosseq 2572  rnuni 2646  imaiun 2650  coass 2667  dmco2 2673  iinon 2948  dfoprab2 3021  domen 3284  xpcomen 3343  xpassen 3344  scott0 3542  aceq5lem1 3558  aceq5lem4 3561  cflem 3700  genpass 3906  addcompr 3917  mulcompr 3919  ltexprlem1 3936  ltexprlem4 3939  reclem1pr 3950  reclem2pr 3951  suplem1pr 3955

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org