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  5511  f1ompt  5786  idref  5880  dff13f  5894  foov  6152  tfr1onlemaccex  6494  tfrcllembxssdm  6502  tfrcllemaccex  6507  oacl  6606  ixpeq2  6859  ixpin  6870  ixpiinm  6871  infmoti  7195  acfun  7389  exmidontriimlem1  7403  exmidontriimlem3  7405  ccfunen  7450  cc2  7453  cc4f  7455  cc4n  7457  cauappcvgprlemladdrl  7844  axcaucvglemres  8086  axpre-suploc  8089  dfinfre  9103  suprzclex  9545  supinfneg  9790  infsupneg  9791  infssuzex  10453  cvg1nlemcau  11495  cvg1nlemres  11496  rexfiuz  11500  recvguniq  11506  resqrexlemglsq  11533  resqrexlemsqa  11535  resqrexlemex  11536  clim0  11796  mertenslem2  12047  bezoutlemmain  12519  ennnfoneleminc  12982  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemr  12994  ctinfom  12999  isnsg2  13740  isbasis2g  14719  tgval2  14725  ntreq0  14806  lmres  14922  eltx  14933  suplociccreex  15298  lgseisenlem2  15750  decidi  16159  nninfsellemqall  16381  nninfomni  16385  trirec0xor  16413