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

Theorem rexbii 2417
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 2413 . 2 (⊤ → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓))
43mptru 1323 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wtru 1315  wrex 2392
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-rex 2397
This theorem is referenced by:  2rexbii  2419  r19.29r  2545  r19.42v  2563  rexcom13  2571  rexrot4  2572  3reeanv  2576  cbvrex2v  2638  rexcom4  2681  rexcom4a  2682  rexcom4b  2683  ceqsrex2v  2789  reu7  2850  0el  3353  iuncom  3787  iuncom4  3788  iuniin  3791  dfiunv2  3817  iunab  3827  iunin2  3844  iundif2ss  3846  iunun  3859  iunxiun  3862  iunpwss  3872  inuni  4048  iunopab  4171  sucel  4300  iunpw  4369  xpiundi  4565  xpiundir  4566  reliin  4629  rexxpf  4654  iunxpf  4655  cnvuni  4693  dmiun  4716  dfima3  4852  rniun  4917  dminxp  4951  imaco  5012  coiun  5016  isarep1  5177  rexrn  5523  ralrn  5524  elrnrexdmb  5526  fnasrn  5564  fnasrng  5566  foima2  5619  rexima  5622  ralima  5623  abrexco  5626  imaiun  5627  fliftcnv  5662  abrexex2g  5984  abrexex2  5988  tfr1onlemaccex  6211  tfrcllemaccex  6224  tfrcldm  6226  qsid  6460  eroveu  6486  ixp0  6591  infmoti  6881  eldju  6919  genpdflem  7279  genpassl  7296  genpassu  7297  nqprm  7314  nqprrnd  7315  ltnqpr  7365  ltnqpri  7366  ltexprlemm  7372  ltexprlemopl  7373  ltexprlemopu  7375  caucvgprprlemaddq  7480  caucvgprprlem1  7481  suplocexprlemml  7488  suplocexprlemloc  7493  caucvgsrlemgt1  7567  elreal  7600  axcaucvglemres  7671  axpre-suploc  7674  dfinfre  8674  suprzclex  9103  supinfneg  9342  infsupneg  9343  ublbneg  9357  4fvwrd4  9868  caucvgre  10704  rexanuz  10711  rexfiuz  10712  resqrexlemglsq  10745  resqrexlemsqa  10747  resqrexlemex  10748  rersqreu  10751  clim0  11005  cbvsum  11080  fsum3  11107  mertenslem2  11256  divalgb  11529  infssuzex  11549  bezoutlemmain  11593  bezoutlemex  11596  ennnfoneleminc  11830  ennnfonelemex  11833  ennnfonelemr  11842  tgval2  12126  ntreq0  12207  metrest  12581
  Copyright terms: Public domain W3C validator