ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexcom4 GIF version

Theorem rexcom4 2643
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 2532 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥𝐴 𝜑)
2 rexv 2638 . . 3 (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
32rexbii 2386 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑥𝐴𝑦𝜑)
4 rexv 2638 . 2 (∃𝑦 ∈ V ∃𝑥𝐴 𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 209 1 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wex 1427  wrex 2361  Vcvv 2620
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-rex 2366  df-v 2622
This theorem is referenced by:  rexcom4a  2644  reuind  2821  iuncom4  3743  dfiun2g  3768  iunn0m  3796  iunxiun  3816  iinexgm  3996  inuni  3997  iunopab  4117  xpiundi  4509  xpiundir  4510  cnvuni  4635  dmiun  4658  elres  4761  elsnres  4762  rniun  4855  imaco  4949  coiun  4953  fun11iun  5287  abrexco  5552  imaiun  5553  fliftf  5592  rexrnmpt2  5774  oprabrexex2  5915  releldm2  5969  eroveu  6397  genpassl  7144  genpassu  7145  ltexprlemopl  7221  ltexprlemopu  7223  ntreq0  11893
  Copyright terms: Public domain W3C validator