Theorem ralbii 2537

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

Syntax hints:   <-> wb 105   T. wtru 1398   A.wral 2509

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-ral 2514

This theorem is referenced by:  2ralbii  2539  ralinexa  2558  r3al  2575  r19.26-2  2661  r19.26-3  2662  ralbiim  2666  r19.28av  2668  ralnex2  2671  ralrot3  2697  cbvral2vw  2777  cbvral2v  2779  cbvral3v  2781  sbralie  2784  ralcom4  2824  reu8  3001  2reuswapdc  3009  r19.12sn  3736  eqsnm  3839  uni0b  3919  uni0c  3920  ssint  3945  iuniin  3981  iuneq2  3987  iunss  4012  ssiinf  4021  iinab  4033  iindif2m  4039  iinin2m  4040  iinuniss  4054  sspwuni  4056  iinpw  4062  dftr3  4192  trint  4203  bnd2  4265  reusv3  4559  reg2exmidlema  4634  setindel  4638  ordsoexmid  4662  zfregfr  4674  tfi  4682  tfis2f  4684  ssrel2  4818  reliun  4850  xpiindim  4869  ralxpf  4878  dfse2  5111  rninxp  5182  dminxp  5183  cnviinm  5280  cnvpom  5281  cnvsom  5282  dffun9  5357  funco  5368  funcnv3  5394  fncnv  5398  funimaexglem  5415  fnres  5451  fnopabg  5458  mptfng  5460  fintm  5524  f1ompt  5801  idref  5902  dff13f  5916  foov  6174  tfr1onlemaccex  6519  tfrcllembxssdm  6527  tfrcllemaccex  6532  oacl  6633  ixpeq2  6886  ixpin  6897  ixpiinm  6898  infmoti  7232  acfun  7427  exmidontriimlem1  7441  exmidontriimlem3  7443  ccfunen  7488  cc2  7491  cc4f  7493  cc4n  7495  cauappcvgprlemladdrl  7882  axcaucvglemres  8124  axpre-suploc  8127  dfinfre  9141  suprzclex  9583  supinfneg  9834  infsupneg  9835  infssuzex  10499  cvg1nlemcau  11567  cvg1nlemres  11568  rexfiuz  11572  recvguniq  11578  resqrexlemglsq  11605  resqrexlemsqa  11607  resqrexlemex  11608  clim0  11868  mertenslem2  12120  bezoutlemmain  12592  ennnfoneleminc  13055  ennnfonelemex  13058  ennnfonelemhom  13059  ennnfonelemr  13067  ctinfom  13072  isnsg2  13813  isbasis2g  14798  tgval2  14804  ntreq0  14885  lmres  15001  eltx  15012  suplociccreex  15377  lgseisenlem2  15829  vtxd0nedgbfi  16179  decidi  16452  nninfsellemqall  16680  nninfomni  16684  trirec0xor  16716