Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
Alternate definition of substitution
nfsb4ALT
Metamath Proof Explorer
Description: Alternate version of nfsb4 . (Contributed by NM , 14-May-1993)
(Revised by Mario Carneiro , 4-Oct-2016)
(Proof modification is discouraged.) (New usage is discouraged.)
Ref
Expression
Hypotheses
dfsb1.p5
⊢ θ ↔ x = y → φ ∧ ∃ x x = y ∧ φ
nfsb4ALT.1
⊢ Ⅎ z φ
Assertion
nfsb4ALT
⊢ ¬ ∀ z z = y → Ⅎ z θ
Proof
Step
Hyp
Ref
Expression
1
dfsb1.p5
⊢ θ ↔ x = y → φ ∧ ∃ x x = y ∧ φ
2
nfsb4ALT.1
⊢ Ⅎ z φ
3
1
nfsb4tALT
⊢ ∀ x Ⅎ z φ → ¬ ∀ z z = y → Ⅎ z θ
4
3 2
mpg
⊢ ¬ ∀ z z = y → Ⅎ z θ