Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Unordered pairs
Interchangeable setvar variables
ichn
Next ⟩
ichim
Metamath Proof Explorer
Ascii
Unicode
Theorem
ichn
Description:
Negation does not affect interchangeability.
(Contributed by
SN
, 30-Aug-2023)
Ref
Expression
Assertion
ichn
⊢
a
⇄
b
φ
↔
a
⇄
b
¬
φ
Proof
Step
Hyp
Ref
Expression
1
notbi
⊢
a
u
b
a
u
b
φ
↔
φ
↔
¬
a
u
b
a
u
b
φ
↔
¬
φ
2
sbn
⊢
u
b
¬
φ
↔
¬
u
b
φ
3
2
sbbii
⊢
b
a
u
b
¬
φ
↔
b
a
¬
u
b
φ
4
sbn
⊢
b
a
¬
u
b
φ
↔
¬
b
a
u
b
φ
5
3
4
bitri
⊢
b
a
u
b
¬
φ
↔
¬
b
a
u
b
φ
6
5
sbbii
⊢
a
u
b
a
u
b
¬
φ
↔
a
u
¬
b
a
u
b
φ
7
sbn
⊢
a
u
¬
b
a
u
b
φ
↔
¬
a
u
b
a
u
b
φ
8
6
7
bitri
⊢
a
u
b
a
u
b
¬
φ
↔
¬
a
u
b
a
u
b
φ
9
8
bibi1i
⊢
a
u
b
a
u
b
¬
φ
↔
¬
φ
↔
¬
a
u
b
a
u
b
φ
↔
¬
φ
10
1
9
bitr4i
⊢
a
u
b
a
u
b
φ
↔
φ
↔
a
u
b
a
u
b
¬
φ
↔
¬
φ
11
10
2albii
⊢
∀
a
∀
b
a
u
b
a
u
b
φ
↔
φ
↔
∀
a
∀
b
a
u
b
a
u
b
¬
φ
↔
¬
φ
12
df-ich
⊢
a
⇄
b
φ
↔
∀
a
∀
b
a
u
b
a
u
b
φ
↔
φ
13
df-ich
⊢
a
⇄
b
¬
φ
↔
∀
a
∀
b
a
u
b
a
u
b
¬
φ
↔
¬
φ
14
11
12
13
3bitr4i
⊢
a
⇄
b
φ
↔
a
⇄
b
¬
φ