MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexcom4 Structured version   Visualization version   GIF version

Theorem rexcom4 3270
Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.)
Assertion
Ref Expression
rexcom4 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rexcom4
StepHypRef Expression
1 exdistr 1959 . 2 (∃𝑥𝑦(𝑥𝐴𝜑) ↔ ∃𝑥(𝑥𝐴 ∧ ∃𝑦𝜑))
2 df-rex 3071 . . . 4 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
32exbii 1851 . . 3 (∃𝑦𝑥𝐴 𝜑 ↔ ∃𝑦𝑥(𝑥𝐴𝜑))
4 excom 2163 . . 3 (∃𝑦𝑥(𝑥𝐴𝜑) ↔ ∃𝑥𝑦(𝑥𝐴𝜑))
53, 4bitri 275 . 2 (∃𝑦𝑥𝐴 𝜑 ↔ ∃𝑥𝑦(𝑥𝐴𝜑))
6 df-rex 3071 . 2 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑥(𝑥𝐴 ∧ ∃𝑦𝜑))
71, 5, 63bitr4ri 304 1 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-11 2155
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3071
This theorem is referenced by:  rexcomOLD  3273  rexcom4a  3274  2ex2rexrot  3280  reuind  3712  uni0b  4895  iuncom4  4963  dfiun2g  4991  dfiun2gOLD  4992  iunn0  5028  iunxiun  5058  iinexg  5299  inuni  5301  iunopab  5517  iunopabOLD  5518  xpiundi  5703  xpiundir  5704  cnvuni  5843  dmiun  5870  dmopab2rex  5874  elsnres  5978  rniun  6101  xpdifid  6121  imaco  6204  coiun  6209  abrexco  7192  imaiun  7193  fliftf  7261  imaeqsexv  7309  imaeqexov  7593  fiun  7876  f1iun  7877  oprabrexex2  7912  releldm2  7976  oarec  8510  omeu  8533  eroveu  8754  brttrcl2  9655  dfac5lem2  10065  genpass  10950  supaddc  12127  supadd  12128  supmul1  12129  supmullem2  12131  supmul  12132  pceu  16723  4sqlem12  16833  mreiincl  17481  psgneu  19293  ntreq0  22444  unisngl  22894  metrest  23896  metuel2  23937  nosupno  27067  nosupfv  27070  noinfno  27082  noinffv  27085  elold  27221  lrrecfr  27277  sleadd1  27320  addsunif  27332  addsasslem1  27333  addsasslem2  27334  istrkg2ld  27444  fpwrelmapffslem  31696  omssubaddlem  32956  omssubadd  32957  bnj906  33599  satfdm  34020  dmopab3rexdif  34056  bj-elsngl  35485  bj-restn0  35607  ismblfin  36165  itg2addnclem3  36177  sdclem1  36248  eldmqs1cossres  37167  prter2  37389  lshpsmreu  37617  islpln5  38044  islvol5  38088  cdlemftr3  39074  mapdpglem3  40184  hdmapglem7a  40436  diophrex  41141  imaiun1  42011  coiun1  42012  grumnudlem  42653  upbdrech  43626
  Copyright terms: Public domain W3C validator