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

Theorem elintg 4266
Description: Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.)
Assertion
Ref Expression
elintg  |-  ( A  e.  V  ->  ( A  e.  |^| B  <->  A. x  e.  B  A  e.  x ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    V( x)

Proof of Theorem elintg
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eleq1 2501 . 2  |-  ( y  =  A  ->  (
y  e.  |^| B  <->  A  e.  |^| B ) )
2 eleq1 2501 . . 3  |-  ( y  =  A  ->  (
y  e.  x  <->  A  e.  x ) )
32ralbidv 2871 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  x  <->  A. x  e.  B  A  e.  x ) )
4 vex 3090 . . 3  |-  y  e. 
_V
54elint2 4265 . 2  |-  ( y  e.  |^| B  <->  A. x  e.  B  y  e.  x )
61, 3, 5vtoclbg 3146 1  |-  ( A  e.  V  ->  ( A  e.  |^| B  <->  A. x  e.  B  A  e.  x ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1870   A.wral 2782   |^|cint 4258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-v 3089  df-int 4259
This theorem is referenced by:  elinti  4267  elrint  4300  onmindif  5531  onmindif2  6653  mremre  15452  toponmre  20031  1stcfb  20382  uffixfr  20860  plycpn  23101  insiga  28789  dfon2lem8  30214  trintALTVD  36907  trintALT  36908  intsaluni  37725  intsal  37726
  Copyright terms: Public domain W3C validator