Metamath Proof Explorer

Theorem clelsb1fw

Description: Substitution for the first argument of the membership predicate in an atomic formula (class version of elsb1 ). Version of clelsb1f with a disjoint variable condition, which does not require ax-13 . (Contributed by Rodolfo Medina, 28-Apr-2010) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 clelsb1fw.1 ⊢ Ⅎ _ x A
2 1 nfcri ⊢ Ⅎ x w ∈ A
3 2 sbco2v ⊢ y x x w w ∈ A ↔ y w w ∈ A
4 clelsb1 ⊢ x w w ∈ A ↔ x ∈ A
5 4 sbbii ⊢ y x x w w ∈ A ↔ y x x ∈ A
6 clelsb1 ⊢ y w w ∈ A ↔ y ∈ A
7 3 5 6 3bitr3i ⊢ y x x ∈ A ↔ y ∈ A