Theorem rabbida3

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

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

Proof

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