Theorem sp 1509

Description: Specialization. Another name for ax-4 1508. (Contributed by NM, 21-May-2008.)

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

Step	Hyp	Ref	Expression
1		ax-4 1508	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-4 1508

This theorem is referenced by:  axi12  1512  nfr  1516  sps  1535  spsd  1536  19.3  1552  cbv1h  1744  nfald  1758  dveeq2  1813  nfsbxy  1940  nfsbxyt  1941  nfcr  2309  nfabdw  2336  rsp  2522  ceqex  2862  abidnf  2903  mob2  2915  csbie2t  3103  sbcnestgf  3106  mpteq12f  4078  dtruarb  4186  copsex2t  4239  ssopab2  4269  eusv1  4446  alxfr  4455  eunex  4554  iota1  5184  fiintim  6918  genprndl  7495  genprndu  7496  fiinopn  13073  bdel  14157  bdsepnft  14199  strcollnft  14296