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

Theorem rexbii 2385
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 2381 . 2  |-  ( T. 
->  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
)
43mptru 1298 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   T. wtru 1290   E.wrex 2360
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-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-rex 2365
This theorem is referenced by:  2rexbii  2387  r19.29r  2507  r19.42v  2524  rexcom13  2532  rexrot4  2533  3reeanv  2537  cbvrex2v  2599  rexcom4  2642  rexcom4a  2643  rexcom4b  2644  ceqsrex2v  2747  reu7  2808  0el  3303  iuncom  3731  iuncom4  3732  iuniin  3735  dfiunv2  3761  iunab  3771  iunin2  3788  iundif2ss  3790  iunun  3803  iunxiun  3805  iunpwss  3812  inuni  3983  iunopab  4099  sucel  4228  iunpw  4292  xpiundi  4484  xpiundir  4485  reliin  4547  rexxpf  4571  iunxpf  4572  cnvuni  4610  dmiun  4633  dfima3  4764  rniun  4829  dminxp  4862  imaco  4923  coiun  4927  isarep1  5086  rexrn  5420  ralrn  5421  elrnrexdmb  5423  fnasrn  5459  fnasrng  5461  foima2  5512  rexima  5516  ralima  5517  abrexco  5520  imaiun  5521  fliftcnv  5556  abrexex2g  5873  abrexex2  5877  tfr1onlemaccex  6095  tfrcllemaccex  6108  tfrcldm  6110  qsid  6337  eroveu  6363  infmoti  6702  eldju  6738  genpdflem  7045  genpassl  7062  genpassu  7063  nqprm  7080  nqprrnd  7081  ltnqpr  7131  ltnqpri  7132  ltexprlemm  7138  ltexprlemopl  7139  ltexprlemopu  7141  caucvgprprlemaddq  7246  caucvgprprlem1  7247  caucvgsrlemgt1  7319  elreal  7345  axcaucvglemres  7413  dfinfre  8389  suprzclex  8814  supinfneg  9052  infsupneg  9053  ublbneg  9067  4fvwrd4  9516  caucvgre  10379  rexanuz  10386  rexfiuz  10387  resqrexlemglsq  10420  resqrexlemsqa  10422  resqrexlemex  10423  rersqreu  10426  clim0  10637  cbvsum  10713  fisum  10742  divalgb  11007  infssuzex  11027  bezoutlemmain  11069  bezoutlemex  11072
  Copyright terms: Public domain W3C validator