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

Theorem elintg 4418
 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 2676 . . 3 (𝑦 = 𝐴 → (𝑦𝑥𝐴𝑥))
21ralbidv 2969 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝑥 ↔ ∀𝑥𝐵 𝐴𝑥))
3 dfint2 4412 . 2 𝐵 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝑥}
42, 3elab2g 3322 1 (𝐴𝑉 → (𝐴 𝐵 ↔ ∀𝑥𝐵 𝐴𝑥))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∩ cint 4410 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-int 4411 This theorem is referenced by:  elinti  4420  elrint  4453  onmindif  5732  onmindif2  6904  mremre  16087  toponmre  20707  1stcfb  21058  uffixfr  21537  plycpn  23848  insiga  29527  dfon2lem8  30939  elintabg  36899  trintALTVD  38138  trintALT  38139  elintd  38271  intsaluni  39223  intsal  39224
 Copyright terms: Public domain W3C validator