Metamath Proof Explorer

Theorem clelsb3fOLD

Description: Obsolete version of clelsb3f as of 7-May-2023. (Contributed by Rodolfo Medina, 28-Apr-2010) (Proof shortened by Andrew Salmon, 14-Jun-2011) (Revised by Thierry Arnoux, 13-Mar-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis clelsb3f.1 ⊢ Ⅎ _ x A
Assertion clelsb3fOLD ⊢ y x x ∈ A ↔ y ∈ A

Proof

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