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

Theorem elintg 4887
Description: Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.)
Assertion
Ref Expression
elintg (𝐴𝑉 → (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem elintg
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eleq1 2826 . . 3 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
21ralbidv 3112 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥))
3 dfint2 4881 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
42, 3elab2g 3611 1 (𝐴𝑉 → (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1539  wcel 2106  wral 3064   cint 4879
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-int 4880
This theorem is referenced by:  elinti  4888  elrint  4922  onmindif  6355  onmindif2  7657  mremre  17313  toponmre  22244  1stcfb  22596  uffixfr  23074  plycpn  25449  insiga  32105  dfon2lem8  33766  elintabg  41182  trintALTVD  42500  trintALT  42501  elintd  42624  intsaluni  43868  intsal  43869
  Copyright terms: Public domain W3C validator