Theorem ralbidv 2326

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 1421	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	ralbid 2324	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 98   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311

This theorem is referenced by:  ralbii  2330  2ralbidv  2348  rexralbidv  2350  r19.32vdc  2459  raleqbi1dv  2513  raleqbidv  2517  cbvral2v  2541  rspc2  2661  rspc3v  2665  reu6i  2732  reu7  2736  sbcralt  2834  sbcralg  2836  raaanlem  3326  r19.12sn  3436  2ralunsn  3569  elintg  3623  elintrabg  3628  eliin  3662  bnd2  3926  poeq1  4036  soeq1  4052  frforeq1  4080  frforeq3  4084  frirrg  4087  frind  4089  weeq1  4093  reusv3  4192  ontr2exmid  4250  reg2exmidlema  4259  posng  4412  ralxpf  4482  cnvpom  4860  funcnvuni  4968  dff4im  5313  dff13f  5409  eusvobj2  5498  ofreq  5715  smoeq  5905  recseq  5921  tfr0  5937  tfrlemiex  5945  nneneq  6320  ac6sfi  6352  elinp  6572  prloc  6589  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgpr  6780  caucvgprpr  6810  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  caucvgsr  6886  axcaucvglemcau  6972  axcaucvglemres  6973  nnsub  7952  indstr  8536  ublbneg  8548  lbzbi  8551  iccsupr  8835  cau4  9712  caubnd2  9713  clim  9802  clim2  9804  clim2c  9805  clim0c  9807  climabs0  9828  cn1lem  9834  sqrt2irr  9878  bj-omtrans  10081