Theorem rexab2

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by Gino Giotto, 1-Dec-2023)

	Ref	Expression
Hypothesis	ralab2.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
Assertion	rexab2	⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜓 ↔ ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralab2.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
2		df-rex	⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜓 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ∧ 𝜓 ) )
3		nfsab1	⊢ Ⅎ 𝑦 𝑥 ∈ { 𝑦 ∣ 𝜑 }
4		nfv	⊢ Ⅎ 𝑦 𝜓
5	3 4	nfan	⊢ Ⅎ 𝑦 ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ∧ 𝜓 )
6		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝜒 )
7		eleq1ab	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ 𝜑 } ) )
8		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
9	7 8	bitrdi	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 ) )
10	9 1	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜒 ) ) )
11	5 6 10	cbvexv1	⊢ ( ∃ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ∧ 𝜓 ) ↔ ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )
12	2 11	bitri	⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜓 ↔ ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )