Metamath Proof Explorer

Theorem clelsb3vOLD

Description: Obsolete version of clelsb3 as of 29-Jul-2023. (Contributed by Wolf Lammen, 30-Apr-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 sbco2vv ⊢ y x x w w ∈ A ↔ y w w ∈ A
2 eleq1w ⊢ w = x → w ∈ A ↔ x ∈ A
3 2 sbievw ⊢ x w w ∈ A ↔ x ∈ A
4 3 sbbii ⊢ y x x w w ∈ A ↔ y x x ∈ A
5 eleq1w ⊢ w = y → w ∈ A ↔ y ∈ A
6 5 sbievw ⊢ y w w ∈ A ↔ y ∈ A
7 1 4 6 3bitr3i ⊢ y x x ∈ A ↔ y ∈ A