Theorem ralbidv 2635

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 2633	1 |- (ph -> (A.x e. A ps <-> A.x e. A ch))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 2620

This theorem is referenced by:  ralbii  2639  2ralbidv  2657  rexralbidv  2659  raleqbi1dv  2816  raleqbidv  2820  cbvral2v  2844  rspc2  2961  rspc3v  2965  reu6i  3028  reu7  3032  sbcralt  3119  sbcralg  3121  raaan  3658  raaanv  3659  r19.12sn  3790  2ralunsn  3881  elintg  3935  elintrabg  3940  eliin  3975  nndisjeq  4430  evenodddisjlem1  4516  evenodddisj  4517  nnpweq  4524  ralxpf  4828  funcnvuni  5162  dff4  5422  dff13f  5473  trd  5922  extd  5924  trrd  5926  refrd  5927  refd  5928  nclenn  6250  nnc3n3p1  6279  nchoicelem12  6301  nchoicelem16  6305  nchoicelem17  6306  nchoicelem19  6308