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

Theorem rexcom4 2623
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  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Distinct variable groups:    x, y    y, A
Allowed substitution hints:    ph( x, y)    A( x)

Proof of Theorem rexcom4
StepHypRef Expression
1 rexcom 2519 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 2618 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2374 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 2618 . 2  |-  ( E. y  e.  _V  E. x  e.  A  ph  <->  E. y E. x  e.  A  ph )
51, 3, 43bitr3i 208 1  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   E.wex 1422   E.wrex 2350   _Vcvv 2602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604
This theorem is referenced by:  rexcom4a  2624  reuind  2796  iuncom4  3687  dfiun2g  3712  iunn0m  3740  iunxiun  3759  iinexgm  3931  inuni  3932  iunopab  4038  xpiundi  4418  xpiundir  4419  cnvuni  4543  dmiun  4566  elres  4668  elsnres  4669  rniun  4758  imaco  4850  coiun  4854  fun11iun  5172  abrexco  5424  imaiun  5425  fliftf  5464  rexrnmpt2  5641  oprabrexex2  5782  releldm2  5836  eroveu  6256  genpassl  6765  genpassu  6766  ltexprlemopl  6842  ltexprlemopu  6844
  Copyright terms: Public domain W3C validator