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 3063 . 2 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
42, 3bitr4i 278 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wcel 2107  wral 3062  Vcvv 3475   cint 4951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-int 4952
This theorem is referenced by:  int0  4967  ssint  4969  intssuni  4975  iinuni  5102  onint  7778  intwun  10730  inttsk  10769  intgru  10809  subgint  19030  subrgint  20342  lssintcl  20575  toponmre  22597  alexsubALTlem3  23553  shintcli  30613  chintcli  30615  intlidl  32567  fin2so  36523  intidl  36945  mzpincl  41520  elimaint  42448  elintima  42452  intsal  45094  salgencntex  45107  subrngint  46787
  Copyright terms: Public domain W3C validator