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

Theorem rexcom4 2683
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 2572 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 2678 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2419 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 2678 . 2  |-  ( E. y  e.  _V  E. x  e.  A  ph  <->  E. y E. x  e.  A  ph )
51, 3, 43bitr3i 209 1  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   E.wex 1453   E.wrex 2394   _Vcvv 2660
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662
This theorem is referenced by:  rexcom4a  2684  reuind  2862  iuncom4  3790  dfiun2g  3815  iunn0m  3843  iunxiun  3864  iinexgm  4049  inuni  4050  iunopab  4173  xpiundi  4567  xpiundir  4568  cnvuni  4695  dmiun  4718  elres  4825  elsnres  4826  rniun  4919  imaco  5014  coiun  5018  fun11iun  5356  abrexco  5628  imaiun  5629  fliftf  5668  rexrnmpo  5854  oprabrexex2  5996  releldm2  6051  eroveu  6488  genpassl  7300  genpassu  7301  ltexprlemopl  7377  ltexprlemopu  7379  ntreq0  12228  metrest  12602
  Copyright terms: Public domain W3C validator