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 ⊢yxA∈x↔A∈y

Proof

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