Theorem ralbii 2372

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 2368	. 2 |- ( T. -> ( A. x e. A ph <-> A. x e. A ps ) )
4	3	trud 1293	1 |- ( A. x e. A ph <-> A. x e. A ps )

Syntax hints:   <-> wb 103   T. wtru 1285   A.wral 2348

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 1376  ax-gen 1378  ax-4 1440  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-ral 2353

This theorem is referenced by:  2ralbii  2374  ralinexa  2393  r3al  2408  r19.26-2  2486  r19.26-3  2487  ralbiim  2491  r19.28av  2493  cbvral2v  2585  cbvral3v  2587  sbralie  2590  ralcom4  2621  reu8  2788  2reuswapdc  2794  r19.12sn  3458  eqsnm  3547  uni0b  3626  uni0c  3627  ssint  3652  iuniin  3688  iuneq2  3694  iunss  3719  ssiinf  3727  iinab  3739  iindif2m  3745  iinin2m  3746  iinuniss  3758  sspwuni  3760  iinpw  3763  dftr3  3879  trint  3890  bnd2  3947  reusv3  4210  reg2exmidlema  4277  setindel  4281  ordsoexmid  4305  zfregfr  4316  tfi  4323  tfis2f  4325  ssrel2  4448  reliun  4476  xpiindim  4491  ralxpf  4500  dfse2  4718  rninxp  4784  dminxp  4785  cnviinm  4879  cnvpom  4880  cnvsom  4881  dffun9  4950  funco  4960  funcnv3  4981  fncnv  4985  funimaexglem  5002  fnres  5035  fnopabg  5042  mptfng  5044  fintm  5095  f1ompt  5341  idref  5417  dff13f  5430  foov  5667  oacl  6063  infmoti  6441  cauappcvgprlemladdrl  6847  axcaucvglemres  7065  dfinfre  8034  suprzclex  8445  supinfneg  8683  infsupneg  8684  cvg1nlemcau  9870  cvg1nlemres  9871  rexfiuz  9875  recvguniq  9881  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  clim0  10124  infssuzex  10345  bezoutlemmain  10387