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

Theorem rexcom4 2577
 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 2474 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥𝐴 𝜑)
2 rexv 2572 . . 3 (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
32rexbii 2331 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑥𝐴𝑦𝜑)
4 rexv 2572 . 2 (∃𝑦 ∈ V ∃𝑥𝐴 𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 199 1 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
 Colors of variables: wff set class Syntax hints:   ↔ wb 98  ∃wex 1381  ∃wrex 2307  Vcvv 2557 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559 This theorem is referenced by:  rexcom4a  2578  reuind  2744  iuncom4  3664  dfiun2g  3689  iunn0m  3717  iunxiun  3736  iinexgm  3908  inuni  3909  iunopab  4018  xpiundi  4398  xpiundir  4399  cnvuni  4521  dmiun  4544  elres  4646  elsnres  4647  rniun  4734  imaco  4826  coiun  4830  fun11iun  5147  abrexco  5398  imaiun  5399  fliftf  5439  rexrnmpt2  5616  oprabrexex2  5757  releldm2  5811  eroveu  6197  genpassl  6622  genpassu  6623  ltexprlemopl  6699  ltexprlemopu  6701
 Copyright terms: Public domain W3C validator