Theorem eleq2w

Description: Weaker version of eleq2 (but more general than elequ2 ) not depending on ax-ext nor df-cleq . (Contributed by BJ, 29-Sep-2019)

	Ref	Expression
Assertion	eleq2w	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
2	1	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥 ) ↔ ( 𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦 ) ) )
3	2	exbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦 ) ) )
4		dfclel	⊢ ( 𝐴 ∈ 𝑥 ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑥 ) )
5		dfclel	⊢ ( 𝐴 ∈ 𝑦 ↔ ∃ 𝑧 ( 𝑧 = 𝐴 ∧ 𝑧 ∈ 𝑦 ) )
6	3 4 5	3bitr4g	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )