Theorem abbii

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)

	Ref	Expression
Hypothesis	abbii.1	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	abbii	⊢ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		abbii.1	⊢ ( 𝜑 ↔ 𝜓 )
2		abbi1	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )
3	2 1	mpg	⊢ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 }