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

Theorem elint2 4855
 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 4854 . 2 (𝐴 𝐵 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
3 df-ral 3130 . 2 (∀𝑥𝐵 𝐴𝑥 ↔ ∀𝑥(𝑥𝐵𝐴𝑥))
42, 3bitr4i 280 1 (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114  ∀wral 3125  Vcvv 3470  ∩ cint 4848 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-int 4849 This theorem is referenced by:  int0  4862  ssint  4864  intssuni  4870  iinuni  4992  onint  7484  intwun  10131  inttsk  10170  intgru  10210  subgint  18278  subrgint  19529  lssintcl  19708  toponmre  21673  alexsubALTlem3  22629  shintcli  29087  chintcli  29089  fin2so  34916  intidl  35339  mzpincl  39464  elimaint  40124  elintima  40129  intsal  42757  salgencntex  42770
 Copyright terms: Public domain W3C validator