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

Theorem rexbii 2442
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 2438 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43mptru 1340 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   T. wtru 1332   E.wrex 2417
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-rex 2422
This theorem is referenced by:  2rexbii  2444  r19.29r  2570  r19.42v  2588  rexcom13  2596  rexrot4  2597  3reeanv  2601  cbvrex2v  2666  rexcom4  2709  rexcom4a  2710  rexcom4b  2711  ceqsrex2v  2817  reu7  2879  0el  3385  iuncom  3819  iuncom4  3820  iuniin  3823  dfiunv2  3849  iunab  3859  iunin2  3876  iundif2ss  3878  iunun  3891  iunxiun  3894  iunpwss  3904  inuni  4080  iunopab  4203  sucel  4332  iunpw  4401  xpiundi  4597  xpiundir  4598  reliin  4661  rexxpf  4686  iunxpf  4687  cnvuni  4725  dmiun  4748  dfima3  4884  rniun  4949  dminxp  4983  imaco  5044  coiun  5048  isarep1  5209  rexrn  5557  ralrn  5558  elrnrexdmb  5560  fnasrn  5598  fnasrng  5600  foima2  5653  rexima  5656  ralima  5657  abrexco  5660  imaiun  5661  fliftcnv  5696  abrexex2g  6018  abrexex2  6022  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfrcldm  6260  qsid  6494  eroveu  6520  ixp0  6625  infmoti  6915  eldju  6953  genpdflem  7322  genpassl  7339  genpassu  7340  nqprm  7357  nqprrnd  7358  ltnqpr  7408  ltnqpri  7409  ltexprlemm  7415  ltexprlemopl  7416  ltexprlemopu  7418  caucvgprprlemaddq  7523  caucvgprprlem1  7524  suplocexprlemml  7531  suplocexprlemloc  7536  caucvgsrlemgt1  7610  elreal  7643  axcaucvglemres  7714  axpre-suploc  7717  dfinfre  8721  suprzclex  9156  supinfneg  9397  infsupneg  9398  ublbneg  9412  4fvwrd4  9924  caucvgre  10760  rexanuz  10767  rexfiuz  10768  resqrexlemglsq  10801  resqrexlemsqa  10803  resqrexlemex  10804  rersqreu  10807  clim0  11061  cbvsum  11136  fsum3  11163  mertenslem2  11312  cbvprod  11334  divalgb  11629  infssuzex  11649  bezoutlemmain  11693  bezoutlemex  11696  ennnfoneleminc  11931  ennnfonelemex  11934  ennnfonelemr  11943  tgval2  12230  ntreq0  12311  metrest  12685
  Copyright terms: Public domain W3C validator