Theorem ralbii 2500

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

Syntax hints:   <-> wb 105   T. wtru 1365   A.wral 2472

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-ral 2477

This theorem is referenced by:  2ralbii  2502  ralinexa  2521  r3al  2538  r19.26-2  2623  r19.26-3  2624  ralbiim  2628  r19.28av  2630  ralnex2  2633  ralrot3  2659  cbvral2vw  2737  cbvral2v  2739  cbvral3v  2741  sbralie  2744  ralcom4  2782  reu8  2956  2reuswapdc  2964  r19.12sn  3684  eqsnm  3781  uni0b  3860  uni0c  3861  ssint  3886  iuniin  3922  iuneq2  3928  iunss  3953  ssiinf  3962  iinab  3974  iindif2m  3980  iinin2m  3981  iinuniss  3995  sspwuni  3997  iinpw  4003  dftr3  4131  trint  4142  bnd2  4202  reusv3  4491  reg2exmidlema  4566  setindel  4570  ordsoexmid  4594  zfregfr  4606  tfi  4614  tfis2f  4616  ssrel2  4749  reliun  4780  xpiindim  4799  ralxpf  4808  dfse2  5038  rninxp  5109  dminxp  5110  cnviinm  5207  cnvpom  5208  cnvsom  5209  dffun9  5283  funco  5294  funcnv3  5316  fncnv  5320  funimaexglem  5337  fnres  5370  fnopabg  5377  mptfng  5379  fintm  5439  f1ompt  5709  idref  5799  dff13f  5813  foov  6065  tfr1onlemaccex  6401  tfrcllembxssdm  6409  tfrcllemaccex  6414  oacl  6513  ixpeq2  6766  ixpin  6777  ixpiinm  6778  infmoti  7087  acfun  7267  exmidontriimlem1  7281  exmidontriimlem3  7283  ccfunen  7324  cc2  7327  cc4f  7329  cc4n  7331  cauappcvgprlemladdrl  7717  axcaucvglemres  7959  axpre-suploc  7962  dfinfre  8975  suprzclex  9415  supinfneg  9660  infsupneg  9661  cvg1nlemcau  11128  cvg1nlemres  11129  rexfiuz  11133  recvguniq  11139  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  clim0  11428  mertenslem2  11679  infssuzex  12086  bezoutlemmain  12135  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemr  12580  ctinfom  12585  isnsg2  13273  isbasis2g  14213  tgval2  14219  ntreq0  14300  lmres  14416  eltx  14427  suplociccreex  14778  lgseisenlem2  15187  decidi  15287  nninfsellemqall  15505  nninfomni  15509  trirec0xor  15535