Theorem rspcv 2952

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
rspcv	⊢ (A ∈ B → (∀x ∈ B φ → ψ))

Distinct variable groups:   x,A   x,B   ψ,x

Allowed substitution hint:   φ(x)

Proof of Theorem rspcv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxψ
2		rspcv.1	. 2 ⊢ (x = A → (φ ↔ ψ))
3	1, 2	rspc 2950	1 ⊢ (A ∈ B → (∀x ∈ B φ → ψ))

Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642   ∈ wcel 1710  ∀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-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620  df-v 2862

This theorem is referenced by:  rspccv  2953  rspcva  2954  rspccva  2955  rspc3v  2965  rr19.3v  2981  rr19.28v  2982  rspsbc  3125  intmin  3947  evenodddisj  4517  nnadjoin  4521  tfinnn  4535  spfinsfincl  4540  funcnvuni  5162  nnc3n3p1  6279  nchoicelem12  6301  nchoicelem19  6308