Theorem ralbidv 2368

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
ralbidv	|- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem ralbidv

Step	Hyp	Ref	Expression
1		nfv 1461	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	ralbid 2366	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 103   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353

This theorem is referenced by:  ralbii  2372  2ralbidv  2390  rexralbidv  2392  r19.32vdc  2503  raleqbi1dv  2557  raleqbidv  2561  cbvral2v  2585  rspc2  2711  rspc3v  2716  reu6i  2783  reu7  2787  sbcralt  2890  sbcralg  2892  raaanlem  3346  2ralunsn  3590  elintg  3644  elintrabg  3649  eliin  3683  bnd2  3947  poeq1  4054  soeq1  4070  frforeq1  4098  frforeq3  4102  frirrg  4105  frind  4107  weeq1  4111  reusv3  4210  ontr2exmid  4268  reg2exmidlema  4277  posng  4430  ralxpf  4500  cnvpom  4880  funcnvuni  4988  dff4im  5334  dff13f  5430  eusvobj2  5518  ofreq  5735  smoeq  5928  recseq  5944  tfr0  5960  tfrlemiex  5968  nneneq  6343  ac6sfi  6379  supeq1  6399  supeq3  6403  supmoti  6406  eqsupti  6409  supubti  6412  suplubti  6413  supisoex  6422  cnvinfex  6431  eqinfti  6433  infvalti  6435  elinp  6664  prloc  6681  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgpr  6872  caucvgprpr  6902  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  caucvgsr  6978  axcaucvglemcau  7064  axcaucvglemres  7065  lbreu  8023  nnsub  8077  indstr  8681  supinfneg  8683  infsupneg  8684  ublbneg  8698  lbzbi  8701  iccsupr  8989  bccl  9694  cau4  10002  caubnd2  10003  maxleast  10099  rexanre  10106  rexico  10107  fimaxre2  10109  minmax  10112  clim  10120  clim2  10122  clim2c  10123  clim0c  10125  climabs0  10146  cn1lem  10152  zsupcllemstep  10341  infssuzex  10345  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemeu  10396  dfgcd3  10399  bezout  10400  dfgcd2  10403  sqrt2irr  10541  bj-omtrans  10751