Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
Axiom scheme ax-12 (Substitution)
nfsbvOLD
Metamath Proof Explorer
Description: Obsolete version of nfsbv as of 13-Aug-2023. (Contributed by Wolf
Lammen , 7-Feb-2023) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypothesis
nfsbv.nf
⊢ Ⅎ z φ
Assertion
nfsbvOLD
⊢ Ⅎ z y x φ
Proof
Step
Hyp
Ref
Expression
1
nfsbv.nf
⊢ Ⅎ z φ
2
sb6
⊢ y x φ ↔ ∀ x x = y → φ
3
nfv
⊢ Ⅎ z x = y
4
3 1
nfim
⊢ Ⅎ z x = y → φ
5
4
nfal
⊢ Ⅎ z ∀ x x = y → φ
6
2 5
nfxfr
⊢ Ⅎ z y x φ