Theorem ra4 1243

Description: Restricted specialization.

Assertion

Ref	Expression
ra4	⊢ (∀x ∈ A φ → (x ∈ A → φ))

Proof of Theorem ra4

Step	Hyp	Ref	Expression
1		df-ral 1205	. 2 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
2		ax-4 673	. 2 ⊢ (∀x(x ∈ A → φ) → (x ∈ A → φ))
3	1, 2	sylbi 174	1 ⊢ (∀x ∈ A φ → (x ∈ A → φ))

Syntax hints:   → wi 2  ∀wal 672   ∈ wcel 1092  ∀wral 1201

This theorem is referenced by:  ra42 1245  rspec 1246  r19.12 1281  r19.15 1292  ss2iun 2005  iineq2 2007  trss 2050  peano5 2394  fnopabg 2745  chfnrn 2885  fopab2 2891  ffnfv 2892  iunon 2947  iinon 2948  tfrlem1 2949  tfrlem9 2957  tfr3 2964  tz7.48-1 2994  tz7.49 2997  nneneq 3408  r1tr 3498  scottex 3541  aceq6b 3565

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673

This theorem depends on definitions:  df-bi 128  df-ral 1205

metamath.org