Theorem eleq1ab

Description: Extension (in the sense of Remark 3 of the comment of df-clab ) of elequ1 from formulas of the form "setvar e. setvar" to formulas of the form "setvar e. class abstraction". This extension does not require ax-8 contrary to elequ1 , but recall from Remark 3 of the comment of df-clab that it can be considered an extension only because of cvjust , which does require ax-8 .

This is an instance of eleq1w where the containing class is a class abstraction, and contrary to it, it can be proved without df-clel . See also eleq1 for general classes.

The straightforward yet important fact that this statement can be proved from FOL= plus df-clab (hence without ax-ext , df-cleq or df-clel ) was stressed by Mario Carneiro. (Contributed by BJ, 17-Aug-2023)

	Ref	Expression
Assertion	eleq1ab	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑧 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑧 ∣ 𝜑 } ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑧 ] 𝜑 ) )
2		df-clab	⊢ ( 𝑥 ∈ { 𝑧 ∣ 𝜑 } ↔ [ 𝑥 / 𝑧 ] 𝜑 )
3		df-clab	⊢ ( 𝑦 ∈ { 𝑧 ∣ 𝜑 } ↔ [ 𝑦 / 𝑧 ] 𝜑 )
4	1 2 3	3bitr4g	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑧 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑧 ∣ 𝜑 } ) )