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

Theorem elintab 4519
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 4513 . 2 (𝐴 {𝑥𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦))
3 nfsab1 2641 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
4 nfv 1883 . . . 4 𝑥 𝐴𝑦
53, 4nfim 1865 . . 3 𝑥(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦)
6 nfv 1883 . . 3 𝑦(𝜑𝐴𝑥)
7 eleq1 2718 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2639 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8syl6bb 276 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
10 eleq2 2719 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
119, 10imbi12d 333 . . 3 (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ (𝜑𝐴𝑥)))
125, 6, 11cbval 2307 . 2 (∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ ∀𝑥(𝜑𝐴𝑥))
132, 12bitri 264 1 (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521  wcel 2030  {cab 2637  Vcvv 3231   cint 4507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-int 4508
This theorem is referenced by:  elintrab  4520  intmin4  4538  intab  4539  intid  4956  dfom3  8582  dfom5  8585  tc2  8656  dfnn2  11071  brintclab  13786  efgi  18178  efgi2  18184  mclsax  31592  heibor1lem  33738  elmapintab  38219  intabssd  38233  cotrintab  38238  dffrege76  38550
  Copyright terms: Public domain W3C validator