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

Theorem elint2 4958
Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999.)
Hypothesis
Ref Expression
elint2.1 𝐴 ∈ V
Assertion
Ref Expression
elint2 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem elint2
StepHypRef Expression
1 elint2.1 . . 3 𝐴 ∈ V
21elint 4957 . 2 (𝐴 𝐵 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
3 df-ral 3060 . 2 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
42, 3bitr4i 278 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  wcel 2106  wral 3059  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-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-int 4952
This theorem is referenced by:  int0  4967  ssint  4969  intssuni  4975  iinuni  5103  onint  7810  intwun  10773  inttsk  10812  intgru  10852  subgint  19181  subrngint  20577  subrgint  20612  lssintcl  20980  toponmre  23117  alexsubALTlem3  24073  shintcli  31358  chintcli  31360  intlidl  33428  fin2so  37594  intidl  38016  mzpincl  42722  elimaint  43639  elintima  43643  intsal  46286  salgencntex  46299
  Copyright terms: Public domain W3C validator