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

Theorem elint2 4957
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 4956 . 2 (𝐴 𝐵 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
3 df-ral 3061 . 2 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
42, 3bitr4i 278 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1538  wcel 2105  wral 3060  Vcvv 3473   cint 4950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-int 4951
This theorem is referenced by:  int0  4966  ssint  4968  intssuni  4974  iinuni  5101  onint  7782  intwun  10736  inttsk  10775  intgru  10815  subgint  19073  subrngint  20456  subrgint  20493  lssintcl  20807  toponmre  22917  alexsubALTlem3  23873  shintcli  31015  chintcli  31017  intlidl  32976  fin2so  36939  intidl  37361  mzpincl  41935  elimaint  42863  elintima  42867  intsal  45505  salgencntex  45518
  Copyright terms: Public domain W3C validator