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

Theorem rexcom4 3236
 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 df-rex 3131 . 2 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑥(𝑥𝐴 ∧ ∃𝑦𝜑))
2 19.42v 1954 . . . . 5 (∃𝑦(𝑥𝐴𝜑) ↔ (𝑥𝐴 ∧ ∃𝑦𝜑))
32bicomi 226 . . . 4 ((𝑥𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦(𝑥𝐴𝜑))
43exbii 1848 . . 3 (∃𝑥(𝑥𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑥𝑦(𝑥𝐴𝜑))
5 excom 2169 . . . 4 (∃𝑥𝑦(𝑥𝐴𝜑) ↔ ∃𝑦𝑥(𝑥𝐴𝜑))
6 df-rex 3131 . . . . . 6 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76bicomi 226 . . . . 5 (∃𝑥(𝑥𝐴𝜑) ↔ ∃𝑥𝐴 𝜑)
87exbii 1848 . . . 4 (∃𝑦𝑥(𝑥𝐴𝜑) ↔ ∃𝑦𝑥𝐴 𝜑)
95, 8bitri 277 . . 3 (∃𝑥𝑦(𝑥𝐴𝜑) ↔ ∃𝑦𝑥𝐴 𝜑)
104, 9bitri 277 . 2 (∃𝑥(𝑥𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦𝑥𝐴 𝜑)
111, 10bitri 277 1 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3126 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2161 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3131 This theorem is referenced by:  2ex2rexrot  3237  rexcom4a  3238  rexcom  3342  reuind  3724  uni0b  4840  iuncom4  4903  dfiun2g  4931  dfiun2gOLD  4932  iunn0  4965  iunxiun  4995  iinexg  5220  inuni  5222  iunopab  5422  xpiundi  5598  xpiundir  5599  cnvuni  5733  dmiun  5758  dmopab2rex  5762  elsnres  5868  rniun  5982  xpdifid  6001  imaco  6080  coiun  6085  abrexco  6980  imaiun  6981  fliftf  7045  fiun  7622  f1iun  7623  oprabrexex2  7657  releldm2  7720  oarec  8166  omeu  8189  eroveu  8370  dfac5lem2  9528  genpass  10409  supaddc  11586  supadd  11587  supmul1  11588  supmullem2  11590  supmul  11591  pceu  16161  4sqlem12  16270  mreiincl  16846  psgneu  18613  ntreq0  21661  unisngl  22111  metrest  23110  metuel2  23151  istrkg2ld  26233  fpwrelmapffslem  30455  omssubaddlem  31565  omssubadd  31566  bnj906  32210  satfdm  32624  dmopab3rexdif  32660  nosupno  33211  nosupfv  33214  bj-elsngl  34297  bj-restn0  34398  ismblfin  34974  itg2addnclem3  34986  sdclem1  35057  eldmqs1cossres  35929  prter2  36053  lshpsmreu  36281  islpln5  36707  islvol5  36751  cdlemftr3  37737  mapdpglem3  38847  hdmapglem7a  39099  diophrex  39509  imaiun1  40131  coiun1  40132  grumnudlem  40776  upbdrech  41726
 Copyright terms: Public domain W3C validator