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

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

Proof of Theorem elintab
StepHypRef Expression
1 elintab.ex . 2 𝐴 ∈ V
2 elintabg 4962 . 2 (𝐴 ∈ V → (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥)))
31, 2ax-mp 5 1 (𝐴 {𝑥𝜑} ↔ ∀𝑥(𝜑𝐴𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  wcel 2106  {cab 2712  Vcvv 3478   cint 4951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-int 4952
This theorem is referenced by:  elintrab  4965  intmin4  4982  intab  4983  intidOLD  5469  dfom3  9685  dfom5  9688  tc2  9780  dfnn2  12277  brintclab  15037  efgi  19752  efgi2  19758  dfn0s2  28351  mclsax  35554  heibor1lem  37796  intabssd  43509  elmapintab  43586  cotrintab  43604  dffrege76  43929
  Copyright terms: Public domain W3C validator