Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Unordered pairs
Interchangeable setvar variables
nfich1
Next ⟩
nfich2
Metamath Proof Explorer
Ascii
Unicode
Theorem
nfich1
Description:
The first interchangeable setvar variable is not free.
(Contributed by
AV
, 21-Aug-2023)
Ref
Expression
Assertion
nfich1
⊢
Ⅎ
x
x
⇄
y
φ
Proof
Step
Hyp
Ref
Expression
1
df-ich
⊢
x
⇄
y
φ
↔
∀
x
∀
y
x
a
y
x
a
y
φ
↔
φ
2
nfa1
⊢
Ⅎ
x
∀
x
∀
y
x
a
y
x
a
y
φ
↔
φ
3
1
2
nfxfr
⊢
Ⅎ
x
x
⇄
y
φ