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

Theorem elintab 4787
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 4782 . 2 (𝐴 {𝑥𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦))
3 nfsab1 2782 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
4 nfv 1890 . . . 4 𝑥 𝐴𝑦
53, 4nfim 1876 . . 3 𝑥(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦)
6 nfv 1890 . . 3 𝑦(𝜑𝐴𝑥)
7 eleq1w 2863 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2777 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8syl6bb 288 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
10 eleq2w 2864 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
119, 10imbi12d 346 . . 3 (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ (𝜑𝐴𝑥)))
125, 6, 11cbvalv1 2318 . 2 (∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ ∀𝑥(𝜑𝐴𝑥))
132, 12bitri 276 1 (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1518  wcel 2079  {cab 2773  Vcvv 3432   cint 4776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-int 4777
This theorem is referenced by:  elintrab  4788  intmin4  4805  intab  4806  intid  5235  dfom3  8945  dfom5  8948  tc2  9019  dfnn2  11488  brintclab  14183  efgi  18560  efgi2  18566  mclsax  32369  heibor1lem  34565  intabssd  39321  elmapintab  39392  cotrintab  39410  dffrege76  39721
  Copyright terms: Public domain W3C validator