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

Theorem rexbii 2331
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 (𝜑𝜓)
Assertion
Ref Expression
rexbii (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)

Proof of Theorem rexbii
StepHypRef Expression
1 ralbii.1 . . . 4 (𝜑𝜓)
21a1i 9 . . 3 (⊤ → (𝜑𝜓))
32rexbidv 2327 . 2 (⊤ → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓))
43trud 1252 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1244  wrex 2307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-rex 2312
This theorem is referenced by:  2rexbii  2333  r19.29r  2451  r19.42v  2467  rexcom13  2475  rexrot4  2476  3reeanv  2480  cbvrex2v  2542  rexcom4  2577  rexcom4a  2578  rexcom4b  2579  ceqsrex2v  2676  reu7  2736  0el  3241  iuncom  3663  iuncom4  3664  iuniin  3667  dfiunv2  3693  iunab  3703  iunin2  3720  iundif2ss  3722  iunun  3734  iunxiun  3736  iunpwss  3743  inuni  3909  iunopab  4018  sucel  4147  iunpw  4211  xpiundi  4398  xpiundir  4399  reliin  4459  rexxpf  4483  iunxpf  4484  cnvuni  4521  dmiun  4544  dfima3  4671  rniun  4734  dminxp  4765  imaco  4826  coiun  4830  isarep1  4985  rexrn  5304  ralrn  5305  elrnrexdmb  5307  fnasrn  5341  fnasrng  5343  rexima  5394  ralima  5395  abrexco  5398  imaiun  5399  fliftcnv  5435  abrexex2g  5747  abrexex2  5751  qsid  6171  eroveu  6197  genpdflem  6603  genpassl  6620  genpassu  6621  nqprm  6638  nqprrnd  6639  ltnqpr  6689  ltnqpri  6690  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemopu  6699  caucvgprprlemaddq  6804  caucvgprprlem1  6805  caucvgsrlemgt1  6877  elreal  6903  axcaucvglemres  6971  ublbneg  8546  4fvwrd4  8995  caucvgre  9554  rexanuz  9561  resqrexlemglsq  9594  resqrexlemsqa  9596  resqrexlemex  9597  rersqreu  9600  clim0  9780
  Copyright terms: Public domain W3C validator