Theorem ralbii 2539

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

Syntax hints:   <-> wb 105   T. wtru 1399   A.wral 2511

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-ral 2516

This theorem is referenced by:  2ralbii  2541  ralinexa  2560  r3al  2577  r19.26-2  2663  r19.26-3  2664  ralbiim  2668  r19.28av  2670  ralnex2  2673  ralrot3  2699  cbvral2vw  2779  cbvral2v  2781  cbvral3v  2783  sbralie  2786  ralcom4  2826  reu8  3003  2reuswapdc  3011  r19.12sn  3739  eqsnm  3843  uni0b  3923  uni0c  3924  ssint  3949  iuniin  3985  iuneq2  3991  iunss  4016  ssiinf  4025  iinab  4037  iindif2m  4043  iinin2m  4044  iinuniss  4058  sspwuni  4060  iinpw  4066  dftr3  4196  trint  4207  bnd2  4269  reusv3  4563  reg2exmidlema  4638  setindel  4642  ordsoexmid  4666  zfregfr  4678  tfi  4686  tfis2f  4688  ssrel2  4822  reliun  4854  xpiindim  4873  ralxpf  4882  dfse2  5116  rninxp  5187  dminxp  5188  cnviinm  5285  cnvpom  5286  cnvsom  5287  dffun9  5362  funco  5373  funcnv3  5399  fncnv  5403  funimaexglem  5420  fnres  5456  fnopabg  5463  mptfng  5465  fintm  5530  f1ompt  5806  idref  5907  dff13f  5921  foov  6179  tfr1onlemaccex  6557  tfrcllembxssdm  6565  tfrcllemaccex  6570  oacl  6671  ixpeq2  6924  ixpin  6935  ixpiinm  6936  infmoti  7287  acfun  7482  exmidontriimlem1  7496  exmidontriimlem3  7498  ccfunen  7543  cc2  7546  cc4f  7548  cc4n  7550  cauappcvgprlemladdrl  7937  axcaucvglemres  8179  axpre-suploc  8182  dfinfre  9195  suprzclex  9639  supinfneg  9890  infsupneg  9891  infssuzex  10556  cvg1nlemcau  11624  cvg1nlemres  11625  rexfiuz  11629  recvguniq  11635  resqrexlemglsq  11662  resqrexlemsqa  11664  resqrexlemex  11665  clim0  11925  mertenslem2  12177  bezoutlemmain  12649  ennnfoneleminc  13112  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemr  13124  ctinfom  13129  isnsg2  13870  isbasis2g  14856  tgval2  14862  ntreq0  14943  lmres  15059  eltx  15070  suplociccreex  15435  lgseisenlem2  15890  vtxd0nedgbfi  16240  decidi  16513  nninfsellemqall  16741  nninfomni  16745  trirec0xor  16777