Theorem ralbii 2400

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

Syntax hints:   <-> wb 104   T. wtru 1300   A.wral 2375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-ral 2380

This theorem is referenced by:  2ralbii  2402  ralinexa  2421  r3al  2436  r19.26-2  2520  r19.26-3  2521  ralbiim  2525  r19.28av  2527  cbvral2v  2620  cbvral3v  2622  sbralie  2625  ralcom4  2663  reu8  2833  2reuswapdc  2841  r19.12sn  3536  eqsnm  3629  uni0b  3708  uni0c  3709  ssint  3734  iuniin  3770  iuneq2  3776  iunss  3801  ssiinf  3809  iinab  3821  iindif2m  3827  iinin2m  3828  iinuniss  3841  sspwuni  3843  iinpw  3849  dftr3  3970  trint  3981  bnd2  4037  reusv3  4319  reg2exmidlema  4387  setindel  4391  ordsoexmid  4415  zfregfr  4426  tfi  4434  tfis2f  4436  ssrel2  4567  reliun  4598  xpiindim  4614  ralxpf  4623  dfse2  4848  rninxp  4918  dminxp  4919  cnviinm  5016  cnvpom  5017  cnvsom  5018  dffun9  5088  funco  5099  funcnv3  5121  fncnv  5125  funimaexglem  5142  fnres  5175  fnopabg  5182  mptfng  5184  fintm  5244  f1ompt  5503  idref  5590  dff13f  5603  foov  5849  tfr1onlemaccex  6175  tfrcllembxssdm  6183  tfrcllemaccex  6188  oacl  6286  ixpeq2  6536  ixpin  6547  ixpiinm  6548  infmoti  6830  cauappcvgprlemladdrl  7366  axcaucvglemres  7584  dfinfre  8572  suprzclex  9001  supinfneg  9240  infsupneg  9241  cvg1nlemcau  10596  cvg1nlemres  10597  rexfiuz  10601  recvguniq  10607  resqrexlemglsq  10634  resqrexlemsqa  10636  resqrexlemex  10637  clim0  10893  mertenslem2  11144  infssuzex  11437  bezoutlemmain  11479  ennnfoneleminc  11716  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemr  11728  ctinfom  11733  isbasis2g  11994  tgval2  12002  ntreq0  12083  lmres  12198  eltx  12209  decidi  12583  nninfsellemqall  12795  nninfomni  12799