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

Theorem rexbii 2348
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
Hypothesis
Ref Expression
ralbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
rexbii  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )

Proof of Theorem rexbii
StepHypRef Expression
1 ralbii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 9 . . 3  |-  ( T. 
->  ( ph  <->  ps )
)
32rexbidv 2344 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43trud 1268 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 102   T. wtru 1260   E.wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-rex 2329
This theorem is referenced by:  2rexbii  2350  r19.29r  2468  r19.42v  2484  rexcom13  2492  rexrot4  2493  3reeanv  2497  cbvrex2v  2559  rexcom4  2594  rexcom4a  2595  rexcom4b  2596  ceqsrex2v  2699  reu7  2759  0el  3269  iuncom  3691  iuncom4  3692  iuniin  3695  dfiunv2  3721  iunab  3731  iunin2  3748  iundif2ss  3750  iunun  3762  iunxiun  3764  iunpwss  3771  inuni  3937  iunopab  4046  sucel  4175  iunpw  4239  xpiundi  4426  xpiundir  4427  reliin  4487  rexxpf  4511  iunxpf  4512  cnvuni  4549  dmiun  4572  dfima3  4699  rniun  4762  dminxp  4793  imaco  4854  coiun  4858  isarep1  5013  rexrn  5332  ralrn  5333  elrnrexdmb  5335  fnasrn  5369  fnasrng  5371  rexima  5422  ralima  5423  abrexco  5426  imaiun  5427  fliftcnv  5463  abrexex2g  5775  abrexex2  5779  qsid  6202  eroveu  6228  genpdflem  6663  genpassl  6680  genpassu  6681  nqprm  6698  nqprrnd  6699  ltnqpr  6749  ltnqpri  6750  ltexprlemm  6756  ltexprlemopl  6757  ltexprlemopu  6759  caucvgprprlemaddq  6864  caucvgprprlem1  6865  caucvgsrlemgt1  6937  elreal  6963  axcaucvglemres  7031  ublbneg  8645  4fvwrd4  9099  caucvgre  9808  rexanuz  9815  rexfiuz  9816  resqrexlemglsq  9849  resqrexlemsqa  9851  resqrexlemex  9852  rersqreu  9855  clim0  10037  divalgb  10237
  Copyright terms: Public domain W3C validator