Theorem ralbii 2512

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 2506	. 2 |- ( T. -> ( A. x e. A ph <-> A. x e. A ps ) )
4	3	mptru 1382	1 |- ( A. x e. A ph <-> A. x e. A ps )

Syntax hints:   <-> wb 105   T. wtru 1374   A.wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-ral 2489

This theorem is referenced by:  2ralbii  2514  ralinexa  2533  r3al  2550  r19.26-2  2635  r19.26-3  2636  ralbiim  2640  r19.28av  2642  ralnex2  2645  ralrot3  2671  cbvral2vw  2749  cbvral2v  2751  cbvral3v  2753  sbralie  2756  ralcom4  2794  reu8  2969  2reuswapdc  2977  r19.12sn  3699  eqsnm  3796  uni0b  3875  uni0c  3876  ssint  3901  iuniin  3937  iuneq2  3943  iunss  3968  ssiinf  3977  iinab  3989  iindif2m  3995  iinin2m  3996  iinuniss  4010  sspwuni  4012  iinpw  4018  dftr3  4147  trint  4158  bnd2  4218  reusv3  4508  reg2exmidlema  4583  setindel  4587  ordsoexmid  4611  zfregfr  4623  tfi  4631  tfis2f  4633  ssrel2  4766  reliun  4797  xpiindim  4816  ralxpf  4825  dfse2  5056  rninxp  5127  dminxp  5128  cnviinm  5225  cnvpom  5226  cnvsom  5227  dffun9  5301  funco  5312  funcnv3  5337  fncnv  5341  funimaexglem  5358  fnres  5394  fnopabg  5401  mptfng  5403  fintm  5463  f1ompt  5733  idref  5827  dff13f  5841  foov  6095  tfr1onlemaccex  6436  tfrcllembxssdm  6444  tfrcllemaccex  6449  oacl  6548  ixpeq2  6801  ixpin  6812  ixpiinm  6813  infmoti  7132  acfun  7321  exmidontriimlem1  7335  exmidontriimlem3  7337  ccfunen  7378  cc2  7381  cc4f  7383  cc4n  7385  cauappcvgprlemladdrl  7772  axcaucvglemres  8014  axpre-suploc  8017  dfinfre  9031  suprzclex  9473  supinfneg  9718  infsupneg  9719  infssuzex  10378  cvg1nlemcau  11328  cvg1nlemres  11329  rexfiuz  11333  recvguniq  11339  resqrexlemglsq  11366  resqrexlemsqa  11368  resqrexlemex  11369  clim0  11629  mertenslem2  11880  bezoutlemmain  12352  ennnfoneleminc  12815  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemr  12827  ctinfom  12832  isnsg2  13572  isbasis2g  14550  tgval2  14556  ntreq0  14637  lmres  14753  eltx  14764  suplociccreex  15129  lgseisenlem2  15581  decidi  15768  nninfsellemqall  15989  nninfomni  15993  trirec0xor  16021