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

Theorem elintab 4870
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 4865 . 2 (𝐴 {𝑥𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦))
3 nfsab1 2722 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
4 nfv 1922 . . . 4 𝑥 𝐴𝑦
53, 4nfim 1904 . . 3 𝑥(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦)
6 nfv 1922 . . 3 𝑦(𝜑𝐴𝑥)
7 eleq1w 2820 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2718 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8bitrdi 290 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
10 eleq2w 2821 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
119, 10imbi12d 348 . . 3 (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ (𝜑𝐴𝑥)))
125, 6, 11cbvalv1 2341 . 2 (∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ ∀𝑥(𝜑𝐴𝑥))
132, 12bitri 278 1 (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1541  wcel 2110  {cab 2714  Vcvv 3408   cint 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-int 4860
This theorem is referenced by:  elintrab  4871  intmin4  4888  intab  4889  intid  5342  dfom3  9262  dfom5  9265  tc2  9358  dfnn2  11843  brintclab  14564  efgi  19109  efgi2  19115  mclsax  33244  heibor1lem  35704  intabssd  40811  elmapintab  40880  cotrintab  40898  dffrege76  41224
  Copyright terms: Public domain W3C validator