Theorem ralbii 2536

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

Syntax hints:   <-> wb 105   T. wtru 1396   A.wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-ral 2513

This theorem is referenced by:  2ralbii  2538  ralinexa  2557  r3al  2574  r19.26-2  2660  r19.26-3  2661  ralbiim  2665  r19.28av  2667  ralnex2  2670  ralrot3  2696  cbvral2vw  2776  cbvral2v  2778  cbvral3v  2780  sbralie  2783  ralcom4  2822  reu8  2999  2reuswapdc  3007  r19.12sn  3732  eqsnm  3833  uni0b  3913  uni0c  3914  ssint  3939  iuniin  3975  iuneq2  3981  iunss  4006  ssiinf  4015  iinab  4027  iindif2m  4033  iinin2m  4034  iinuniss  4048  sspwuni  4050  iinpw  4056  dftr3  4186  trint  4197  bnd2  4257  reusv3  4551  reg2exmidlema  4626  setindel  4630  ordsoexmid  4654  zfregfr  4666  tfi  4674  tfis2f  4676  ssrel2  4809  reliun  4840  xpiindim  4859  ralxpf  4868  dfse2  5101  rninxp  5172  dminxp  5173  cnviinm  5270  cnvpom  5271  cnvsom  5272  dffun9  5347  funco  5358  funcnv3  5383  fncnv  5387  funimaexglem  5404  fnres  5440  fnopabg  5447  mptfng  5449  fintm  5513  f1ompt  5788  idref  5886  dff13f  5900  foov  6158  tfr1onlemaccex  6500  tfrcllembxssdm  6508  tfrcllemaccex  6513  oacl  6614  ixpeq2  6867  ixpin  6878  ixpiinm  6879  infmoti  7206  acfun  7400  exmidontriimlem1  7414  exmidontriimlem3  7416  ccfunen  7461  cc2  7464  cc4f  7466  cc4n  7468  cauappcvgprlemladdrl  7855  axcaucvglemres  8097  axpre-suploc  8100  dfinfre  9114  suprzclex  9556  supinfneg  9802  infsupneg  9803  infssuzex  10465  cvg1nlemcau  11511  cvg1nlemres  11512  rexfiuz  11516  recvguniq  11522  resqrexlemglsq  11549  resqrexlemsqa  11551  resqrexlemex  11552  clim0  11812  mertenslem2  12063  bezoutlemmain  12535  ennnfoneleminc  12998  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemr  13010  ctinfom  13015  isnsg2  13756  isbasis2g  14735  tgval2  14741  ntreq0  14822  lmres  14938  eltx  14949  suplociccreex  15314  lgseisenlem2  15766  vtxd0nedgbfi  16059  decidi  16242  nninfsellemqall  16469  nninfomni  16473  trirec0xor  16501