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

Theorem rexcom4 2735
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 2621 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥𝐴 𝜑)
2 rexv 2730 . . 3 (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
32rexbii 2464 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑥𝐴𝑦𝜑)
4 rexv 2730 . 2 (∃𝑦 ∈ V ∃𝑥𝐴 𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 209 1 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104  wex 1472  wrex 2436  Vcvv 2712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714
This theorem is referenced by:  rexcom4a  2736  reuind  2917  iuncom4  3858  dfiun2g  3883  iunn0m  3911  iunxiun  3932  iinexgm  4117  inuni  4118  iunopab  4243  xpiundi  4646  xpiundir  4647  cnvuni  4774  dmiun  4797  elres  4904  elsnres  4905  rniun  4998  imaco  5093  coiun  5097  fun11iun  5437  abrexco  5711  imaiun  5712  fliftf  5751  rexrnmpo  5938  oprabrexex2  6080  releldm2  6135  eroveu  6573  genpassl  7446  genpassu  7447  ltexprlemopl  7523  ltexprlemopu  7525  pceu  12185  ntreq0  12602  metrest  12976
  Copyright terms: Public domain W3C validator