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  6624  tfrcllembxssdm  6632  tfrcllemaccex  6637  oacl  6738  ixpeq2  7000  ixpin  7011  ixpiinm  7012  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  9754  supinfneg  10010  infsupneg  10011  infssuzex  10682  hashfibc  11304  cvg1nlemcau  11771  cvg1nlemres  11772  rexfiuz  11776  recvguniq  11782  resqrexlemglsq  11809  resqrexlemsqa  11811  resqrexlemex  11812  clim0  12075  mertenslem2  12327  bezoutlemmain  12799  ballotfilem7  13336  ennnfoneleminc  13359  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemr  13371  ctinfom  13376  isnsg2  14064  psrbagmax  15183  isbasis2g  15288  tgval2  15294  ntreq0  15375  lmres  15491  eltx  15502  suplociccreex  15867  lgseisenlem2  16412  vtxd0nedgbfi  16762  decidi  17045  nninfsellemqall  17281  nninfomni  17285  trirec0xor  17318  ralsbii  17366  ralseubii  17398