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

Theorem rexbii 2419
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 2415 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43mptru 1325 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   T. wtru 1317   E.wrex 2394
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-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-rex 2399
This theorem is referenced by:  2rexbii  2421  r19.29r  2547  r19.42v  2565  rexcom13  2573  rexrot4  2574  3reeanv  2578  cbvrex2v  2640  rexcom4  2683  rexcom4a  2684  rexcom4b  2685  ceqsrex2v  2791  reu7  2852  0el  3355  iuncom  3789  iuncom4  3790  iuniin  3793  dfiunv2  3819  iunab  3829  iunin2  3846  iundif2ss  3848  iunun  3861  iunxiun  3864  iunpwss  3874  inuni  4050  iunopab  4173  sucel  4302  iunpw  4371  xpiundi  4567  xpiundir  4568  reliin  4631  rexxpf  4656  iunxpf  4657  cnvuni  4695  dmiun  4718  dfima3  4854  rniun  4919  dminxp  4953  imaco  5014  coiun  5018  isarep1  5179  rexrn  5525  ralrn  5526  elrnrexdmb  5528  fnasrn  5566  fnasrng  5568  foima2  5621  rexima  5624  ralima  5625  abrexco  5628  imaiun  5629  fliftcnv  5664  abrexex2g  5986  abrexex2  5990  tfr1onlemaccex  6213  tfrcllemaccex  6226  tfrcldm  6228  qsid  6462  eroveu  6488  ixp0  6593  infmoti  6883  eldju  6921  genpdflem  7283  genpassl  7300  genpassu  7301  nqprm  7318  nqprrnd  7319  ltnqpr  7369  ltnqpri  7370  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemopu  7379  caucvgprprlemaddq  7484  caucvgprprlem1  7485  suplocexprlemml  7492  suplocexprlemloc  7497  caucvgsrlemgt1  7571  elreal  7604  axcaucvglemres  7675  axpre-suploc  7678  dfinfre  8682  suprzclex  9117  supinfneg  9358  infsupneg  9359  ublbneg  9373  4fvwrd4  9885  caucvgre  10721  rexanuz  10728  rexfiuz  10729  resqrexlemglsq  10762  resqrexlemsqa  10764  resqrexlemex  10765  rersqreu  10768  clim0  11022  cbvsum  11097  fsum3  11124  mertenslem2  11273  divalgb  11549  infssuzex  11569  bezoutlemmain  11613  bezoutlemex  11616  ennnfoneleminc  11851  ennnfonelemex  11854  ennnfonelemr  11863  tgval2  12147  ntreq0  12228  metrest  12602
  Copyright terms: Public domain W3C validator