Metamath Proof Explorer


Theorem rexrab

Description: Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ralab.1 ( 𝑦 = 𝑥 → ( 𝜑𝜓 ) )
Assertion rexrab ( ∃ 𝑥 ∈ { 𝑦𝐴𝜑 } 𝜒 ↔ ∃ 𝑥𝐴 ( 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 ralab.1 ( 𝑦 = 𝑥 → ( 𝜑𝜓 ) )
2 1 elrab ( 𝑥 ∈ { 𝑦𝐴𝜑 } ↔ ( 𝑥𝐴𝜓 ) )
3 2 anbi1i ( ( 𝑥 ∈ { 𝑦𝐴𝜑 } ∧ 𝜒 ) ↔ ( ( 𝑥𝐴𝜓 ) ∧ 𝜒 ) )
4 anass ( ( ( 𝑥𝐴𝜓 ) ∧ 𝜒 ) ↔ ( 𝑥𝐴 ∧ ( 𝜓𝜒 ) ) )
5 3 4 bitri ( ( 𝑥 ∈ { 𝑦𝐴𝜑 } ∧ 𝜒 ) ↔ ( 𝑥𝐴 ∧ ( 𝜓𝜒 ) ) )
6 5 rexbii2 ( ∃ 𝑥 ∈ { 𝑦𝐴𝜑 } 𝜒 ↔ ∃ 𝑥𝐴 ( 𝜓𝜒 ) )