This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Reduce dependencies on axioms. (Revised by Wolf Lammen, 24-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 eleq2w ⊢ x = z → A ∈ x ↔ A ∈ z
2 eleq2w ⊢ z = y → A ∈ z ↔ A ∈ y
3 1 2 sbievw2 ⊢ y x A ∈ x ↔ A ∈ y