Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Exemplar theorems
Standard replacements of ax-10 , ax-11 , ax-12
nfa1w
Next ⟩
eu6w
Metamath Proof Explorer
Ascii
Unicode
Theorem
nfa1w
Description:
Replace
ax-10
in
nfa1
with a substitution hypothesis.
(Contributed by
SN
, 2-Sep-2025)
Ref
Expression
Hypothesis
nfa1w.x
⊢
x
=
y
→
φ
↔
ψ
Assertion
nfa1w
⊢
Ⅎ
x
∀
x
φ
Proof
Step
Hyp
Ref
Expression
1
nfa1w.x
⊢
x
=
y
→
φ
↔
ψ
2
1
cbvalvw
⊢
∀
x
φ
↔
∀
y
ψ
3
nfv
⊢
Ⅎ
x
∀
y
ψ
4
2
3
nfxfr
⊢
Ⅎ
x
∀
x
φ