Metamath Proof Explorer


Theorem elint

Description: Membership in class intersection. (Contributed by NM, 21-May-1994)

Ref Expression
Hypothesis elint.1 𝐴 ∈ V
Assertion elint ( 𝐴 𝐵 ↔ ∀ 𝑥 ( 𝑥𝐵𝐴𝑥 ) )

Proof

Step Hyp Ref Expression
1 elint.1 𝐴 ∈ V
2 eleq1 ( 𝑦 = 𝐴 → ( 𝑦𝑥𝐴𝑥 ) )
3 2 imbi2d ( 𝑦 = 𝐴 → ( ( 𝑥𝐵𝑦𝑥 ) ↔ ( 𝑥𝐵𝐴𝑥 ) ) )
4 3 albidv ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝑥𝐵𝑦𝑥 ) ↔ ∀ 𝑥 ( 𝑥𝐵𝐴𝑥 ) ) )
5 df-int 𝐵 = { 𝑦 ∣ ∀ 𝑥 ( 𝑥𝐵𝑦𝑥 ) }
6 4 5 elab2g ( 𝐴 ∈ V → ( 𝐴 𝐵 ↔ ∀ 𝑥 ( 𝑥𝐵𝐴𝑥 ) ) )
7 1 6 ax-mp ( 𝐴 𝐵 ↔ ∀ 𝑥 ( 𝑥𝐵𝐴𝑥 ) )