Theorem ralbidv 2320

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

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

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 1333  ax-gen 1335  ax-4 1397  ax-17 1416

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305

This theorem is referenced by:  ralbii  2324  2ralbidv  2342  rexralbidv  2344  r19.32vdc  2453  raleqbi1dv  2507  raleqbidv  2511  cbvral2v  2535  rspc2  2655  rspc3v  2659  reu6i  2726  reu7  2730  sbcralt  2828  sbcralg  2830  raaanlem  3320  r19.12sn  3427  2ralunsn  3560  elintg  3614  elintrabg  3619  eliin  3653  bnd2  3917  poeq1  4027  soeq1  4043  reusv3  4158  posng  4355  ralxpf  4425  cnvpom  4803  funcnvuni  4911  dff4im  5256  dff13f  5352  eusvobj2  5441  ofreq  5657  smoeq  5846  recseq  5862  tfr0  5878  tfrlemiex  5886  elinp  6456  prloc  6473  nnsub  7693  indstr  8272  ublbneg  8284  lbzbi  8287  iccsupr  8565  bj-omtrans  9344