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

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

Proof of Theorem rexcom4
StepHypRef Expression
1 rexcom 3169 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥𝐴 𝜑)
2 rexv 3292 . . 3 (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
32rexbii 3111 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑥𝐴𝑦𝜑)
4 rexv 3292 . 2 (∃𝑦 ∈ V ∃𝑥𝐴 𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 290 1 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1785  wrex 2983  Vcvv 3272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ral 2987  df-rex 2988  df-v 3274
This theorem is referenced by:  rexcom4a  3298  reuind  3485  uni0b  4539  iuncom4  4604  dfiun2g  4628  iunn0  4656  iunxiun  4684  iinexg  4897  inuni  4899  iunopab  5084  xpiundi  5250  xpiundir  5251  cnvuni  5384  dmiun  5408  elres  5513  elsnres  5514  rniun  5621  xpdifid  5640  imaco  5721  coiun  5726  abrexco  6585  imaiun  6586  fliftf  6648  fun11iun  7211  oprabrexex2  7243  releldm2  7305  oarec  7730  omeu  7753  eroveu  7928  dfac5lem2  9028  genpass  9912  supaddc  11071  supadd  11072  supmul1  11073  supmullem2  11075  supmul  11076  pceu  15642  4sqlem12  15751  mreiincl  16347  psgneu  18015  ntreq0  20972  unisngl  21421  metrest  22419  metuel2  22460  istrkg2ld  25447  fpwrelmapffslem  29705  omssubaddlem  30559  omssubadd  30560  bnj906  31196  nosupno  32044  nosupfv  32047  bj-elsngl  33151  bj-restn0  33238  ismblfin  33650  itg2addnclem3  33663  sdclem1  33739  prter2  34555  lshpsmreu  34784  islpln5  35209  islvol5  35253  cdlemftr3  36240  mapdpglem3  37351  hdmapglem7a  37606  diophrex  37726  imaiun1  38330  coiun1  38331  upbdrech  39903
  Copyright terms: Public domain W3C validator