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  4235  trint  4246  bnd2  4312  reusv3  4608  reg2exmidlema  4683  setindel  4687  ordsoexmid  4711  zfregfr  4723  tfi  4731  tfis2f  4733  ssrel2  4867  reliun  4900  xpiindim  4919  ralxpf  4928  dfse2  5163  rninxp  5234  dminxp  5235  cnviinm  5332  cnvpom  5333  cnvsom  5334  dffun9  5409  funco  5420  funcnv3  5446  fncnv  5450  funimaexglem  5467  fnres  5503  fnopabg  5510  mptfng  5512  fintm  5580  f1ompt  5862  idref  5965  dff13f  5979  foov  6239  tfr1onlemaccex  6623  tfrcllembxssdm  6631  tfrcllemaccex  6636  oacl  6737  ixpeq2  6998  ixpin  7009  ixpiinm  7010  infmoti  7374  acfun  7569  exmidontriimlem1  7583  exmidontriimlem3  7585  ccfunen  7636  cc2  7639  cc4f  7641  cc4n  7643  cauappcvgprlemladdrl  8030  axcaucvglemres  8272  axpre-suploc  8275  dfinfre  9294  suprzclex  9755  supinfneg  10011  infsupneg  10012  infssuzex  10683  hashfibc  11305  cvg1nlemcau  11772  cvg1nlemres  11773  rexfiuz  11777  recvguniq  11783  resqrexlemglsq  11810  resqrexlemsqa  11812  resqrexlemex  11813  clim0  12076  mertenslem2  12328  bezoutlemmain  12800  ballotfilem7  13337  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemr  13372  ctinfom  13377  isnsg2  14065  isbasis2g  15271  tgval2  15277  ntreq0  15358  lmres  15474  eltx  15485  suplociccreex  15850  lgseisenlem2  16395  vtxd0nedgbfi  16745  decidi  17028  nninfsellemqall  17264  nninfomni  17268  trirec0xor  17301  ralsbii  17349  ralseubii  17381