Theorem ralbidv 2634

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

Syntax hints:   -> wi 4   <-> wb 176  A.wral 2614

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619

This theorem is referenced by:  ralbii  2638  2ralbidv  2656  rexralbidv  2658  raleqbi1dv  2815  raleqbidv  2819  cbvral2v  2843  rspc2  2960  rspc3v  2964  reu6i  3027  reu7  3031  sbcralt  3118  sbcralg  3120  raaan  3657  raaanv  3658  r19.12sn  3789  2ralunsn  3880  elintg  3934  elintrabg  3939  eliin  3974  nndisjeq  4429  evenodddisjlem1  4515  evenodddisj  4516  nnpweq  4523  ralxpf  4827  funcnvuni  5161  dff4  5421  dff13f  5472  trd  5921  extd  5923  trrd  5925  refrd  5926  refd  5927  nclenn  6249  nnc3n3p1  6278  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  nchoicelem19  6307