Theorem ralbii 2556

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

This proof depends on syntax axioms:   <-> wb 105   T. wtru 1403   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-ral 2533

This theorem is used by:  2ralbii  2558  ralinexa  2577  r3al  2594  r19.26-2  2680  r19.26-3  2681  ralbiim  2685  r19.28av  2687  ralnex2  2690  ralrot3  2716  cbvral2vw  2797  cbvral2v  2799  cbvral3v  2801  sbralie  2804  ralcom4  2844  reu8  3022  2reuswapdc  3030  r19.12sn  3775  eqsnm  3880  uni0b  3960  uni0c  3961  ssint  3986  iuniin  4022  iuneq2  4028  iunss  4053  ssiinf  4062  iinab  4074  iindif2m  4080  iinin2m  4081  iinuniss  4095  sspwuni  4097  iinpw  4103  dftr3  4233  trint  4244  bnd2  4310  reusv3  4606  reg2exmidlema  4681  setindel  4685  ordsoexmid  4709  zfregfr  4721  tfi  4729  tfis2f  4731  ssrel2  4865  reliun  4898  xpiindim  4917  ralxpf  4926  dfse2  5160  rninxp  5231  dminxp  5232  cnviinm  5329  cnvpom  5330  cnvsom  5331  dffun9  5406  funco  5417  funcnv3  5443  fncnv  5447  funimaexglem  5464  fnres  5500  fnopabg  5507  mptfng  5509  fintm  5577  f1ompt  5859  idref  5962  dff13f  5976  foov  6236  tfr1onlemaccex  6619  tfrcllembxssdm  6627  tfrcllemaccex  6632  oacl  6733  ixpeq2  6994  ixpin  7005  ixpiinm  7006  infmoti  7368  acfun  7563  exmidontriimlem1  7577  exmidontriimlem3  7579  ccfunen  7630  cc2  7633  cc4f  7635  cc4n  7637  cauappcvgprlemladdrl  8024  axcaucvglemres  8266  axpre-suploc  8269  dfinfre  9286  suprzclex  9744  supinfneg  9995  infsupneg  9996  infssuzex  10666  hashfibc  11283  cvg1nlemcau  11750  cvg1nlemres  11751  rexfiuz  11755  recvguniq  11761  resqrexlemglsq  11788  resqrexlemsqa  11790  resqrexlemex  11791  clim0  12051  mertenslem2  12303  bezoutlemmain  12775  ballotfilem7  13279  ennnfoneleminc  13302  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemr  13314  ctinfom  13319  isnsg2  14006  isbasis2g  15146  tgval2  15152  ntreq0  15233  lmres  15349  eltx  15360  suplociccreex  15725  lgseisenlem2  16190  vtxd0nedgbfi  16540  decidi  16823  nninfsellemqall  17058  nninfomni  17062  trirec0xor  17094  ralsbii  17142  ralseubii  17174