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

Theorem ralbii 2373
Description: Inference adding restricted universal 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
ralbii  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . . 4  |-  ( ph  <->  ps )
21a1i 9 . . 3  |-  ( T. 
->  ( ph  <->  ps )
)
32ralbidv 2369 . 2  |-  ( T. 
->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
)
43trud 1294 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   T. wtru 1286   A.wral 2349
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-ral 2354
This theorem is referenced by:  2ralbii  2375  ralinexa  2394  r3al  2409  r19.26-2  2487  r19.26-3  2488  ralbiim  2492  r19.28av  2494  cbvral2v  2586  cbvral3v  2588  sbralie  2591  ralcom4  2622  reu8  2789  2reuswapdc  2795  r19.12sn  3466  eqsnm  3555  uni0b  3634  uni0c  3635  ssint  3660  iuniin  3696  iuneq2  3702  iunss  3727  ssiinf  3735  iinab  3747  iindif2m  3753  iinin2m  3754  iinuniss  3766  sspwuni  3768  iinpw  3771  dftr3  3887  trint  3898  bnd2  3955  reusv3  4218  reg2exmidlema  4285  setindel  4289  ordsoexmid  4313  zfregfr  4324  tfi  4331  tfis2f  4333  ssrel2  4456  reliun  4486  xpiindim  4501  ralxpf  4510  dfse2  4728  rninxp  4794  dminxp  4795  cnviinm  4889  cnvpom  4890  cnvsom  4891  dffun9  4960  funco  4970  funcnv3  4992  fncnv  4996  funimaexglem  5013  fnres  5046  fnopabg  5053  mptfng  5055  fintm  5106  f1ompt  5352  idref  5428  dff13f  5441  foov  5678  tfr1onlemaccex  5997  tfrcllembxssdm  6005  tfrcllemaccex  6010  oacl  6104  infmoti  6500  cauappcvgprlemladdrl  6909  axcaucvglemres  7127  dfinfre  8101  suprzclex  8526  supinfneg  8764  infsupneg  8765  cvg1nlemcau  10008  cvg1nlemres  10009  rexfiuz  10013  recvguniq  10019  resqrexlemglsq  10046  resqrexlemsqa  10048  resqrexlemex  10049  clim0  10262  infssuzex  10489  bezoutlemmain  10531  decidi  10756
  Copyright terms: Public domain W3C validator