Theorem sp 1498

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

Assertion

Ref	Expression
sp	⊢ (∀𝑥𝜑 → 𝜑)

Proof of Theorem sp

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

Syntax hints:   → wi 4  ∀wal 1340

This theorem was proved from axioms:  ax-4 1497

This theorem is referenced by:  axi12  1501  nfr  1505  sps  1524  spsd  1525  19.3  1541  cbv1h  1733  nfald  1747  dveeq2  1802  nfsbxy  1929  nfsbxyt  1930  nfcr  2298  nfabdw  2325  rsp  2511  ceqex  2848  abidnf  2889  mob2  2901  csbie2t  3088  sbcnestgf  3091  mpteq12f  4056  dtruarb  4164  copsex2t  4217  ssopab2  4247  eusv1  4424  alxfr  4433  eunex  4532  iota1  5161  fiintim  6885  genprndl  7453  genprndu  7454  fiinopn  12543  bdel  13562  bdsepnft  13604  strcollnft  13701