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

Theorem elintab 4633
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 4628 . 2 (𝐴 {𝑥𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦))
3 nfsab1 2764 . . . 4 𝑥 𝑦 ∈ {𝑥𝜑}
4 nfv 1998 . . . 4 𝑥 𝐴𝑦
53, 4nfim 1980 . . 3 𝑥(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦)
6 nfv 1998 . . 3 𝑦(𝜑𝐴𝑥)
7 eleq1w 2836 . . . . 5 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝑥 ∈ {𝑥𝜑}))
8 abid 2762 . . . . 5 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
97, 8syl6bb 277 . . . 4 (𝑦 = 𝑥 → (𝑦 ∈ {𝑥𝜑} ↔ 𝜑))
10 eleq2w 2837 . . . 4 (𝑦 = 𝑥 → (𝐴𝑦𝐴𝑥))
119, 10imbi12d 334 . . 3 (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ (𝜑𝐴𝑥)))
125, 6, 11cbval 2435 . 2 (∀𝑦(𝑦 ∈ {𝑥𝜑} → 𝐴𝑦) ↔ ∀𝑥(𝜑𝐴𝑥))
132, 12bitri 265 1 (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1632  wcel 2148  {cab 2760  Vcvv 3355   cint 4622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-v 3357  df-int 4623
This theorem is referenced by:  elintrab  4634  intmin4  4651  intab  4652  intid  5068  dfom3  8729  dfom5  8732  tc2  8803  dfnn2  11256  brintclab  13972  efgi  18359  efgi2  18365  mclsax  31821  heibor1lem  33956  elmapintab  38442  intabssd  38456  cotrintab  38461  dffrege76  38773
  Copyright terms: Public domain W3C validator