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

Theorem ralbii 2384
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 2380 . 2  |-  ( T. 
->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
)
43mptru 1298 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   T. wtru 1290   A.wral 2359
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-4 1445  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-ral 2364
This theorem is referenced by:  2ralbii  2386  ralinexa  2405  r3al  2420  r19.26-2  2498  r19.26-3  2499  ralbiim  2503  r19.28av  2505  cbvral2v  2598  cbvral3v  2600  sbralie  2603  ralcom4  2641  reu8  2809  2reuswapdc  2817  r19.12sn  3503  eqsnm  3594  uni0b  3673  uni0c  3674  ssint  3699  iuniin  3735  iuneq2  3741  iunss  3766  ssiinf  3774  iinab  3786  iindif2m  3792  iinin2m  3793  iinuniss  3806  sspwuni  3808  iinpw  3811  dftr3  3932  trint  3943  bnd2  4000  reusv3  4273  reg2exmidlema  4340  setindel  4344  ordsoexmid  4368  zfregfr  4379  tfi  4387  tfis2f  4389  ssrel2  4516  reliun  4546  xpiindim  4561  ralxpf  4570  dfse2  4792  rninxp  4861  dminxp  4862  cnviinm  4959  cnvpom  4960  cnvsom  4961  dffun9  5030  funco  5040  funcnv3  5062  fncnv  5066  funimaexglem  5083  fnres  5116  fnopabg  5123  mptfng  5125  fintm  5180  f1ompt  5434  idref  5518  dff13f  5531  foov  5773  tfr1onlemaccex  6095  tfrcllembxssdm  6103  tfrcllemaccex  6108  oacl  6203  infmoti  6702  cauappcvgprlemladdrl  7195  axcaucvglemres  7413  dfinfre  8389  suprzclex  8814  supinfneg  9052  infsupneg  9053  cvg1nlemcau  10381  cvg1nlemres  10382  rexfiuz  10386  recvguniq  10392  resqrexlemglsq  10419  resqrexlemsqa  10421  resqrexlemex  10422  clim0  10636  infssuzex  11025  bezoutlemmain  11067  decidi  11339  nninfsellemqall  11551  nninfomni  11555
  Copyright terms: Public domain W3C validator