Theorem bj-gabeqis

Description: Equality of generalized class abstractions, with implicit substitution. (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-gabeqis.c	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
	bj-gabeqis.f	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	bj-gabeqis	⊢ { 𝐴 ∣ 𝑥 ∣ 𝜑 } = { 𝐵 ∣ 𝑦 ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		bj-gabeqis.c	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2		bj-gabeqis.f	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3	1	adantl	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐵 )
4		simpl	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑦 ) → 𝑢 = 𝑣 )
5	3 4	eqeq12d	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑦 ) → ( 𝐴 = 𝑢 ↔ 𝐵 = 𝑣 ) )
6	2	adantl	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑦 ) → ( 𝜑 ↔ 𝜓 ) )
7	5 6	anbi12d	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑦 ) → ( ( 𝐴 = 𝑢 ∧ 𝜑 ) ↔ ( 𝐵 = 𝑣 ∧ 𝜓 ) ) )
8	7	cbvexdvaw	⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ( 𝐴 = 𝑢 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝐵 = 𝑣 ∧ 𝜓 ) ) )
9	8	cbvabv	⊢ { 𝑢 ∣ ∃ 𝑥 ( 𝐴 = 𝑢 ∧ 𝜑 ) } = { 𝑣 ∣ ∃ 𝑦 ( 𝐵 = 𝑣 ∧ 𝜓 ) }
10		df-bj-gab	⊢ { 𝐴 ∣ 𝑥 ∣ 𝜑 } = { 𝑢 ∣ ∃ 𝑥 ( 𝐴 = 𝑢 ∧ 𝜑 ) }
11		df-bj-gab	⊢ { 𝐵 ∣ 𝑦 ∣ 𝜓 } = { 𝑣 ∣ ∃ 𝑦 ( 𝐵 = 𝑣 ∧ 𝜓 ) }
12	9 10 11	3eqtr4i	⊢ { 𝐴 ∣ 𝑥 ∣ 𝜑 } = { 𝐵 ∣ 𝑦 ∣ 𝜓 }