This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rexab2

Description: Existential quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by GG, 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 ⊢ ( ∃ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜓 ↔ ∃ 𝑦 ( 𝜑 ∧ 𝜒 ) )