Metamath Proof Explorer

Theorem clelsb2OLD

Description: Obsolete version of clelsb2 as of 24-Nov-2024.) (Contributed by Jim Kingdon, 22-Nov-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion clelsb2OLD ⊢ y x A ∈ x ↔ A ∈ y

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ x A ∈ w
2 1 sbco2 ⊢ y x x w A ∈ w ↔ y w A ∈ w
3 nfv ⊢ Ⅎ w A ∈ x
4 eleq2 ⊢ w = x → A ∈ w ↔ A ∈ x
5 3 4 sbie ⊢ x w A ∈ w ↔ A ∈ x
6 5 sbbii ⊢ y x x w A ∈ w ↔ y x A ∈ x
7 nfv ⊢ Ⅎ w A ∈ y
8 eleq2 ⊢ w = y → A ∈ w ↔ A ∈ y
9 7 8 sbie ⊢ y w A ∈ w ↔ A ∈ y
10 2 6 9 3bitr3i ⊢ y x A ∈ x ↔ A ∈ y