Theorem sp 1511

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-4 1510

This theorem is referenced by:  axi12  1514  nfr  1518  sps  1537  spsd  1538  19.3  1554  cbv1h  1746  nfald  1760  dveeq2  1815  nfsbxy  1942  nfsbxyt  1943  nfcr  2311  nfabdw  2338  rsp  2524  ceqex  2866  abidnf  2907  mob2  2919  csbie2t  3107  sbcnestgf  3110  mpteq12f  4085  dtruarb  4193  copsex2t  4247  ssopab2  4277  eusv1  4454  alxfr  4463  eunex  4562  iota1  5194  fiintim  6930  genprndl  7522  genprndu  7523  fiinopn  13543  bdel  14636  bdsepnft  14678  strcollnft  14775