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	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		eleq2w	⊢ ( 𝑥 = 𝑧 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑧 ) )
2		eleq2w	⊢ ( 𝑧 = 𝑦 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦 ) )
3	1 2	sbievw2	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 )