Theorem bj-elgab

Description: Elements of a generalized class abstraction. (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Hypotheses	bj-elgab.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	bj-elgab.nfa	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	bj-elgab.ex	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	bj-elgab.is	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ↔ 𝜒 ) )
Assertion	bj-elgab	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝐵 ∣ 𝑥 ∣ 𝜓 } ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-elgab.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		bj-elgab.nfa	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
3		bj-elgab.ex	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		bj-elgab.is	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ↔ 𝜒 ) )
5		df-bj-gab	⊢ { 𝐵 ∣ 𝑥 ∣ 𝜓 } = { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) }
6	5	eleq2i	⊢ ( 𝐴 ∈ { 𝐵 ∣ 𝑥 ∣ 𝜓 } ↔ 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) } )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ∀ 𝑥 𝜑 )
8		nfcvd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 )
9		id	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝐴 )
10	8 9	nfeqd	⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝑦 = 𝐴 )
11	10	nf5rd	⊢ ( Ⅎ 𝑥 𝐴 → ( 𝑦 = 𝐴 → ∀ 𝑥 𝑦 = 𝐴 ) )
12	2 11	syl	⊢ ( 𝜑 → ( 𝑦 = 𝐴 → ∀ 𝑥 𝑦 = 𝐴 ) )
13	12	imp	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ∀ 𝑥 𝑦 = 𝐴 )
14		19.26	⊢ ( ∀ 𝑥 ( 𝜑 ∧ 𝑦 = 𝐴 ) ↔ ( ∀ 𝑥 𝜑 ∧ ∀ 𝑥 𝑦 = 𝐴 ) )
15	7 13 14	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ∀ 𝑥 ( 𝜑 ∧ 𝑦 = 𝐴 ) )
16		eqeq2	⊢ ( 𝑦 = 𝐴 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐴 ) )
17		eqcom	⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
18	16 17	bitrdi	⊢ ( 𝑦 = 𝐴 → ( 𝐵 = 𝑦 ↔ 𝐴 = 𝐵 ) )
19	18	anbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝐵 = 𝑦 ∧ 𝜓 ) ↔ ( 𝐴 = 𝐵 ∧ 𝜓 ) ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( ( 𝐵 = 𝑦 ∧ 𝜓 ) ↔ ( 𝐴 = 𝐵 ∧ 𝜓 ) ) )
21	15 20	exbidh	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → ( ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ) )
22	21	ex	⊢ ( 𝜑 → ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ) ) )
23	22	alrimiv	⊢ ( 𝜑 → ∀ 𝑦 ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ) ) )
24		elabgt	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ) ) ) → ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) } ↔ ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ) )
25	3 23 24	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) } ↔ ∃ 𝑥 ( 𝐴 = 𝐵 ∧ 𝜓 ) ) )
26	25 4	bitrd	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) } ↔ 𝜒 ) )
27	6 26	bitrid	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝐵 ∣ 𝑥 ∣ 𝜓 } ↔ 𝜒 ) )