Theorem abeq1

Description: Equality of a class variable and a class abstraction. Commuted form of abeq2 . (Contributed by NM, 20-Aug-1993)

	Ref	Expression
Assertion	abeq1	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		abeq2	⊢ ( 𝐴 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) )
2		eqcom	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ 𝐴 = { 𝑥 ∣ 𝜑 } )
3		bicom	⊢ ( ( 𝜑 ↔ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) )
4	3	albii	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) )
5	1 2 4	3bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 ∈ 𝐴 ) )