Metamath Proof Explorer

Theorem clelsb2

Description: Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 ). (Contributed by Jim Kingdon, 22-Nov-2018)

Ref Expression
Assertion clelsb2 ⊢ 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