Metamath Proof Explorer


Theorem elintabg

Description: Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020)

Ref Expression
Assertion elintabg ( 𝐴𝑉 → ( 𝐴 { 𝑥𝜑 } ↔ ∀ 𝑥 ( 𝜑𝐴𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 elintg ( 𝐴𝑉 → ( 𝐴 { 𝑥𝜑 } ↔ ∀ 𝑦 ∈ { 𝑥𝜑 } 𝐴𝑦 ) )
2 eleq2w ( 𝑦 = 𝑥 → ( 𝐴𝑦𝐴𝑥 ) )
3 2 ralab2 ( ∀ 𝑦 ∈ { 𝑥𝜑 } 𝐴𝑦 ↔ ∀ 𝑥 ( 𝜑𝐴𝑥 ) )
4 1 3 bitrdi ( 𝐴𝑉 → ( 𝐴 { 𝑥𝜑 } ↔ ∀ 𝑥 ( 𝜑𝐴𝑥 ) ) )