Theorem ralbii 2483

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

Syntax hints:   <-> wb 105   T. wtru 1354   A.wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-ral 2460

This theorem is referenced by:  2ralbii  2485  ralinexa  2504  r3al  2521  r19.26-2  2606  r19.26-3  2607  ralbiim  2611  r19.28av  2613  ralnex2  2616  cbvral2vw  2714  cbvral2v  2716  cbvral3v  2718  sbralie  2721  ralcom4  2759  reu8  2933  2reuswapdc  2941  r19.12sn  3658  eqsnm  3755  uni0b  3834  uni0c  3835  ssint  3860  iuniin  3896  iuneq2  3902  iunss  3927  ssiinf  3936  iinab  3948  iindif2m  3954  iinin2m  3955  iinuniss  3969  sspwuni  3971  iinpw  3977  dftr3  4105  trint  4116  bnd2  4173  reusv3  4460  reg2exmidlema  4533  setindel  4537  ordsoexmid  4561  zfregfr  4573  tfi  4581  tfis2f  4583  ssrel2  4716  reliun  4747  xpiindim  4764  ralxpf  4773  dfse2  5001  rninxp  5072  dminxp  5073  cnviinm  5170  cnvpom  5171  cnvsom  5172  dffun9  5245  funco  5256  funcnv3  5278  fncnv  5282  funimaexglem  5299  fnres  5332  fnopabg  5339  mptfng  5341  fintm  5401  f1ompt  5667  idref  5757  dff13f  5770  foov  6020  tfr1onlemaccex  6348  tfrcllembxssdm  6356  tfrcllemaccex  6361  oacl  6460  ixpeq2  6711  ixpin  6722  ixpiinm  6723  infmoti  7026  acfun  7205  exmidontriimlem1  7219  exmidontriimlem3  7221  ccfunen  7262  cc2  7265  cc4f  7267  cc4n  7269  cauappcvgprlemladdrl  7655  axcaucvglemres  7897  axpre-suploc  7900  dfinfre  8911  suprzclex  9349  supinfneg  9593  infsupneg  9594  cvg1nlemcau  10988  cvg1nlemres  10989  rexfiuz  10993  recvguniq  10999  resqrexlemglsq  11026  resqrexlemsqa  11028  resqrexlemex  11029  clim0  11288  mertenslem2  11539  infssuzex  11944  bezoutlemmain  11993  ennnfoneleminc  12406  ennnfonelemex  12409  ennnfonelemhom  12410  ennnfonelemr  12418  ctinfom  12423  isnsg2  13016  isbasis2g  13436  tgval2  13444  ntreq0  13525  lmres  13641  eltx  13652  suplociccreex  13995  decidi  14429  nninfsellemqall  14646  nninfomni  14650  trirec0xor  14675