Metamath Proof Explorer


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 ( ∃ 𝑥 ∈ { 𝑦𝜑 } 𝜓 ↔ ∃ 𝑦 ( 𝜑𝜒 ) )