Theorem rabbida2

Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	rabbida2.1	⊢ Ⅎ 𝑥 𝜑
	rabbida2.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	rabbida2.3	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion	rabbida2	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐵 ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		rabbida2.1	⊢ Ⅎ 𝑥 𝜑
2		rabbida2.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		rabbida2.3	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
4	2	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
5	4 3	anbi12d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) )
6	1 5	abbid	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) } )
7		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
8		df-rab	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜒 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) }
9	6 7 8	3eqtr4g	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∈ 𝐵 ∣ 𝜒 } )