Theorem bj-gabeqd

Description: Equality of generalized class abstractions. Deduction form. (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-gabeqd.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	bj-gabeqd.c	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	bj-gabeqd.f	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion	bj-gabeqd	⊢ ( 𝜑 → { 𝐴 ∣ 𝑥 ∣ 𝜓 } = { 𝐵 ∣ 𝑥 ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		bj-gabeqd.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		bj-gabeqd.c	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		bj-gabeqd.f	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
4	3	biimpd	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
5	1 2 4	bj-gabssd	⊢ ( 𝜑 → { 𝐴 ∣ 𝑥 ∣ 𝜓 } ⊆ { 𝐵 ∣ 𝑥 ∣ 𝜒 } )
6	2	eqcomd	⊢ ( 𝜑 → 𝐵 = 𝐴 )
7	3	biimprd	⊢ ( 𝜑 → ( 𝜒 → 𝜓 ) )
8	1 6 7	bj-gabssd	⊢ ( 𝜑 → { 𝐵 ∣ 𝑥 ∣ 𝜒 } ⊆ { 𝐴 ∣ 𝑥 ∣ 𝜓 } )
9	5 8	eqssd	⊢ ( 𝜑 → { 𝐴 ∣ 𝑥 ∣ 𝜓 } = { 𝐵 ∣ 𝑥 ∣ 𝜒 } )