Theorem ralbii 2503

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

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 |- ( ph <-> ps )
2	1	a1i 9	. . 3 |- ( T. -> ( ph <-> ps ) )
3	2	ralbidv 2497	. 2 |- ( T. -> ( A. x e. A ph <-> A. x e. A ps ) )
4	3	mptru 1373	1 |- ( A. x e. A ph <-> A. x e. A ps )

Syntax hints:   <-> wb 105   T. wtru 1365   A.wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-ral 2480

This theorem is referenced by:  2ralbii  2505  ralinexa  2524  r3al  2541  r19.26-2  2626  r19.26-3  2627  ralbiim  2631  r19.28av  2633  ralnex2  2636  ralrot3  2662  cbvral2vw  2740  cbvral2v  2742  cbvral3v  2744  sbralie  2747  ralcom4  2785  reu8  2960  2reuswapdc  2968  r19.12sn  3689  eqsnm  3786  uni0b  3865  uni0c  3866  ssint  3891  iuniin  3927  iuneq2  3933  iunss  3958  ssiinf  3967  iinab  3979  iindif2m  3985  iinin2m  3986  iinuniss  4000  sspwuni  4002  iinpw  4008  dftr3  4136  trint  4147  bnd2  4207  reusv3  4496  reg2exmidlema  4571  setindel  4575  ordsoexmid  4599  zfregfr  4611  tfi  4619  tfis2f  4621  ssrel2  4754  reliun  4785  xpiindim  4804  ralxpf  4813  dfse2  5043  rninxp  5114  dminxp  5115  cnviinm  5212  cnvpom  5213  cnvsom  5214  dffun9  5288  funco  5299  funcnv3  5321  fncnv  5325  funimaexglem  5342  fnres  5377  fnopabg  5384  mptfng  5386  fintm  5446  f1ompt  5716  idref  5806  dff13f  5820  foov  6074  tfr1onlemaccex  6415  tfrcllembxssdm  6423  tfrcllemaccex  6428  oacl  6527  ixpeq2  6780  ixpin  6791  ixpiinm  6792  infmoti  7103  acfun  7290  exmidontriimlem1  7304  exmidontriimlem3  7306  ccfunen  7347  cc2  7350  cc4f  7352  cc4n  7354  cauappcvgprlemladdrl  7741  axcaucvglemres  7983  axpre-suploc  7986  dfinfre  9000  suprzclex  9441  supinfneg  9686  infsupneg  9687  infssuzex  10340  cvg1nlemcau  11166  cvg1nlemres  11167  rexfiuz  11171  recvguniq  11177  resqrexlemglsq  11204  resqrexlemsqa  11206  resqrexlemex  11207  clim0  11467  mertenslem2  11718  bezoutlemmain  12190  ennnfoneleminc  12653  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemr  12665  ctinfom  12670  isnsg2  13409  isbasis2g  14365  tgval2  14371  ntreq0  14452  lmres  14568  eltx  14579  suplociccreex  14944  lgseisenlem2  15396  decidi  15525  nninfsellemqall  15746  nninfomni  15750  trirec0xor  15776