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

Theorem ralbii 2441
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 2437 . 2  |-  ( T. 
->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
)
43mptru 1340 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   T. wtru 1332   A.wral 2416
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-ral 2421
This theorem is referenced by:  2ralbii  2443  ralinexa  2462  r3al  2477  r19.26-2  2561  r19.26-3  2562  ralbiim  2566  r19.28av  2568  ralnex2  2571  cbvral2v  2665  cbvral3v  2667  sbralie  2670  ralcom4  2708  reu8  2880  2reuswapdc  2888  r19.12sn  3589  eqsnm  3682  uni0b  3761  uni0c  3762  ssint  3787  iuniin  3823  iuneq2  3829  iunss  3854  ssiinf  3862  iinab  3874  iindif2m  3880  iinin2m  3881  iinuniss  3895  sspwuni  3897  iinpw  3903  dftr3  4030  trint  4041  bnd2  4097  reusv3  4381  reg2exmidlema  4449  setindel  4453  ordsoexmid  4477  zfregfr  4488  tfi  4496  tfis2f  4498  ssrel2  4629  reliun  4660  xpiindim  4676  ralxpf  4685  dfse2  4912  rninxp  4982  dminxp  4983  cnviinm  5080  cnvpom  5081  cnvsom  5082  dffun9  5152  funco  5163  funcnv3  5185  fncnv  5189  funimaexglem  5206  fnres  5239  fnopabg  5246  mptfng  5248  fintm  5308  f1ompt  5571  idref  5658  dff13f  5671  foov  5917  tfr1onlemaccex  6245  tfrcllembxssdm  6253  tfrcllemaccex  6258  oacl  6356  ixpeq2  6606  ixpin  6617  ixpiinm  6618  infmoti  6915  acfun  7063  ccfunen  7079  cc2  7082  cc4f  7084  cc4n  7086  cauappcvgprlemladdrl  7472  axcaucvglemres  7714  axpre-suploc  7717  dfinfre  8721  suprzclex  9156  supinfneg  9397  infsupneg  9398  cvg1nlemcau  10763  cvg1nlemres  10764  rexfiuz  10768  recvguniq  10774  resqrexlemglsq  10801  resqrexlemsqa  10803  resqrexlemex  10804  clim0  11061  mertenslem2  11312  infssuzex  11649  bezoutlemmain  11693  ennnfoneleminc  11931  ennnfonelemex  11934  ennnfonelemhom  11935  ennnfonelemr  11943  ctinfom  11948  isbasis2g  12222  tgval2  12230  ntreq0  12311  lmres  12427  eltx  12438  suplociccreex  12781  decidi  13016  nninfsellemqall  13225  nninfomni  13229
  Copyright terms: Public domain W3C validator