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

Theorem elint2 4953
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 4952 . 2 (𝐴 𝐵 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
3 df-ral 3062 . 2 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
42, 3bitr4i 278 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wcel 2108  wral 3061  Vcvv 3480   cint 4946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-int 4947
This theorem is referenced by:  int0  4962  ssint  4964  intssuni  4970  iinuni  5098  onint  7810  intwun  10775  inttsk  10814  intgru  10854  subgint  19168  subrngint  20560  subrgint  20595  lssintcl  20962  toponmre  23101  alexsubALTlem3  24057  shintcli  31348  chintcli  31350  intlidl  33448  fin2so  37614  intidl  38036  mzpincl  42745  elimaint  43662  elintima  43666  intsal  46345  salgencntex  46358
  Copyright terms: Public domain W3C validator