Metamath Proof Explorer


Theorem elintab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993)

Ref Expression
Hypothesis inteqab.1 𝐴 ∈ V
Assertion elintab ( 𝐴 { 𝑥𝜑 } ↔ ∀ 𝑥 ( 𝜑𝐴𝑥 ) )

Proof

Step Hyp Ref Expression
1 inteqab.1 𝐴 ∈ V
2 1 elint ( 𝐴 { 𝑥𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥𝜑 } → 𝐴𝑦 ) )
3 nfsab1 𝑥 𝑦 ∈ { 𝑥𝜑 }
4 nfv 𝑥 𝐴𝑦
5 3 4 nfim 𝑥 ( 𝑦 ∈ { 𝑥𝜑 } → 𝐴𝑦 )
6 nfv 𝑦 ( 𝜑𝐴𝑥 )
7 eleq1w ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥𝜑 } ↔ 𝑥 ∈ { 𝑥𝜑 } ) )
8 abid ( 𝑥 ∈ { 𝑥𝜑 } ↔ 𝜑 )
9 7 8 bitrdi ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥𝜑 } ↔ 𝜑 ) )
10 eleq2w ( 𝑦 = 𝑥 → ( 𝐴𝑦𝐴𝑥 ) )
11 9 10 imbi12d ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ { 𝑥𝜑 } → 𝐴𝑦 ) ↔ ( 𝜑𝐴𝑥 ) ) )
12 5 6 11 cbvalv1 ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥𝜑 } → 𝐴𝑦 ) ↔ ∀ 𝑥 ( 𝜑𝐴𝑥 ) )
13 2 12 bitri ( 𝐴 { 𝑥𝜑 } ↔ ∀ 𝑥 ( 𝜑𝐴𝑥 ) )