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

Theorem elintg 4474
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 2687 . . 3 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
21ralbidv 2983 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥))
3 dfint2 4468 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
42, 3elab2g 3347 1 (𝐴𝑉 → (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  wral 2909   cint 4466
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-v 3197  df-int 4467
This theorem is referenced by:  elinti  4476  elrint  4509  onmindif  5803  onmindif2  6997  mremre  16245  toponmre  20878  1stcfb  21229  uffixfr  21708  plycpn  24025  insiga  30174  dfon2lem8  31669  elintabg  37699  trintALTVD  38936  trintALT  38937  elintd  39065  intsaluni  40310  intsal  40311
  Copyright terms: Public domain W3C validator