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  2957  2reuswapdc  2965  r19.12sn  3685  eqsnm  3782  uni0b  3861  uni0c  3862  ssint  3887  iuniin  3923  iuneq2  3929  iunss  3954  ssiinf  3963  iinab  3975  iindif2m  3981  iinin2m  3982  iinuniss  3996  sspwuni  3998  iinpw  4004  dftr3  4132  trint  4143  bnd2  4203  reusv3  4492  reg2exmidlema  4567  setindel  4571  ordsoexmid  4595  zfregfr  4607  tfi  4615  tfis2f  4617  ssrel2  4750  reliun  4781  xpiindim  4800  ralxpf  4809  dfse2  5039  rninxp  5110  dminxp  5111  cnviinm  5208  cnvpom  5209  cnvsom  5210  dffun9  5284  funco  5295  funcnv3  5317  fncnv  5321  funimaexglem  5338  fnres  5371  fnopabg  5378  mptfng  5380  fintm  5440  f1ompt  5710  idref  5800  dff13f  5814  foov  6067  tfr1onlemaccex  6403  tfrcllembxssdm  6411  tfrcllemaccex  6416  oacl  6515  ixpeq2  6768  ixpin  6779  ixpiinm  6780  infmoti  7089  acfun  7269  exmidontriimlem1  7283  exmidontriimlem3  7285  ccfunen  7326  cc2  7329  cc4f  7331  cc4n  7333  cauappcvgprlemladdrl  7719  axcaucvglemres  7961  axpre-suploc  7964  dfinfre  8977  suprzclex  9418  supinfneg  9663  infsupneg  9664  cvg1nlemcau  11131  cvg1nlemres  11132  rexfiuz  11136  recvguniq  11142  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  clim0  11431  mertenslem2  11682  infssuzex  12089  bezoutlemmain  12138  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemr  12583  ctinfom  12588  isnsg2  13276  isbasis2g  14224  tgval2  14230  ntreq0  14311  lmres  14427  eltx  14438  suplociccreex  14803  lgseisenlem2  15228  decidi  15357  nninfsellemqall  15575  nninfomni  15579  trirec0xor  15605