Metamath Proof Explorer


Theorem elrabiOLD

Description: Obsolete version of elrabi as of 5-Aug-2024. (Contributed by Alexander van der Vekens, 31-Dec-2017) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion elrabiOLD ( 𝐴 ∈ { 𝑥𝑉𝜑 } → 𝐴𝑉 )

Proof

Step Hyp Ref Expression
1 clelab ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥𝑉𝜑 ) } ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥𝑉𝜑 ) ) )
2 eleq1 ( 𝑥 = 𝐴 → ( 𝑥𝑉𝐴𝑉 ) )
3 2 anbi1d ( 𝑥 = 𝐴 → ( ( 𝑥𝑉𝜑 ) ↔ ( 𝐴𝑉𝜑 ) ) )
4 3 simprbda ( ( 𝑥 = 𝐴 ∧ ( 𝑥𝑉𝜑 ) ) → 𝐴𝑉 )
5 4 exlimiv ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ( 𝑥𝑉𝜑 ) ) → 𝐴𝑉 )
6 1 5 sylbi ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥𝑉𝜑 ) } → 𝐴𝑉 )
7 df-rab { 𝑥𝑉𝜑 } = { 𝑥 ∣ ( 𝑥𝑉𝜑 ) }
8 6 7 eleq2s ( 𝐴 ∈ { 𝑥𝑉𝜑 } → 𝐴𝑉 )