Theorem sp 1533

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1370

This theorem was proved from axioms:  ax-4 1532

This theorem is referenced by:  axi12  1536  nfr  1540  sps  1559  spsd  1560  19.3  1576  cbv1h  1768  nfald  1782  dveeq2  1837  nfsbxy  1969  nfsbxyt  1970  nfcr  2339  nfabdw  2366  rsp  2552  ceqex  2899  abidnf  2940  mob2  2952  csbie2t  3141  sbcnestgf  3144  mpteq12f  4123  dtruarb  4234  copsex2t  4288  ssopab2  4320  eusv1  4497  alxfr  4506  eunex  4607  iota1  5243  fiintim  7010  genprndl  7616  genprndu  7617  fiinopn  14394  bdel  15645  bdsepnft  15687  strcollnft  15784