Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elintab Structured version   Visualization version   GIF version

Theorem elintab 4850
 Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
inteqab.1 𝐴 ∈ V
Assertion
Ref Expression
elintab (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elintab
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 inteqab.1 . . 3 𝐴 ∈ V
21elint 4845 . 2 (𝐴 {𝑥𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦))
3 nfsab1 2785 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
4 nfv 1915 . . . 4 𝑥 𝐴𝑦
53, 4nfim 1897 . . 3 𝑥(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦)
6 nfv 1915 . . 3 𝑦(𝜑𝐴𝑥)
7 eleq1w 2872 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2780 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8syl6bb 290 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
10 eleq2w 2873 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
119, 10imbi12d 348 . . 3 (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ (𝜑𝐴𝑥)))
125, 6, 11cbvalv1 2350 . 2 (∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ ∀𝑥(𝜑𝐴𝑥))
132, 12bitri 278 1 (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2111  {cab 2776  Vcvv 3441  ∩ cint 4839 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-int 4840 This theorem is referenced by:  elintrab  4851  intmin4  4868  intab  4869  intid  5316  dfom3  9097  dfom5  9100  tc2  9171  dfnn2  11641  brintclab  14355  efgi  18841  efgi2  18847  mclsax  32944  heibor1lem  35266  intabssd  40270  elmapintab  40339  cotrintab  40357  dffrege76  40683
 Copyright terms: Public domain W3C validator