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

Theorem elin2d 4164
Description: Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
Hypothesis
Ref Expression
elin1d.1 (𝜑𝑋 ∈ (𝐴𝐵))
Assertion
Ref Expression
elin2d (𝜑𝑋𝐵)

Proof of Theorem elin2d
StepHypRef Expression
1 elin1d.1 . 2 (𝜑𝑋 ∈ (𝐴𝐵))
2 elinel2 4161 . 2 (𝑋 ∈ (𝐴𝐵) → 𝑋𝐵)
31, 2syl 17 1 (𝜑𝑋𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cin 3914
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922
This theorem is referenced by:  f1opwfi  9307  elfiun  9373  ordtypelem3  9463  infpwfien  10005  ttukeylem6  10457  fpwwe2lem11  10584  explecnv  15757  bitsinv1  16329  smuval2  16369  firest  17321  sscres  17713  funcres2c  17795  coffth  17830  rescfth  17831  catcoppccl  18010  catcoppcclOLD  18011  catcfuccl  18012  catcfucclOLD  18013  catcxpccl  18102  catcxpcclOLD  18103  psssdm2  18477  sylow2a  19408  frgpnabllem2  19659  sralmod  20672  zringlpirlem3  20901  mplind  21494  neiptoptop  22498  restbas  22525  ordtrest  22569  subbascn  22621  lmss  22665  cnconn  22789  clsconn  22797  conncompclo  22802  subislly  22848  cldllycmp  22862  1stckgenlem  22920  txcls  22971  txcnp  22987  txtube  23007  txcmplem1  23008  txkgen  23019  xkopt  23022  xkococnlem  23026  txconn  23056  basqtop  23078  tgqtop  23079  kqnrmlem1  23110  kqnrmlem2  23111  nrmhmph  23161  uzrest  23264  alexsubALTlem3  23416  ptcmplem2  23420  tsmslem1  23496  tsmsxplem1  23520  tsmsxplem2  23521  tsmsxp  23522  blin2  23798  met2ndci  23894  zdis  24195  reconnlem2  24206  reconn  24207  xrge0gsumle  24212  cnheibor  24334  lebnum  24343  nmoleub2lem3  24494  nmoleub3  24498  caussi  24677  minveclem4b  24811  minveclem4  24812  ovolfcl  24846  ovolfioo  24847  ovolficc  24848  ovolficcss  24849  ovolfsval  24850  ovoliunlem1  24882  ovolicc2lem4  24900  ovolicc2lem5  24901  uniiccdif  24958  uniioovol  24959  uniiccvol  24960  uniioombllem2a  24962  uniioombllem3a  24964  uniioombllem4  24966  uniioombllem5  24967  uniioombllem6  24968  vitalilem2  24989  vitalilem4  24991  ig1peu  25552  taylfvallem1  25732  tayl0  25737  ppisval  26469  chtf  26473  efchtcl  26476  chtge0  26477  ppinprm  26517  chtprm  26518  chtnprm  26519  chtwordi  26521  chtdif  26523  efchtdvds  26524  chtlepsi  26570  chtleppi  26574  pclogsum  26579  chpval2  26582  chpchtsum  26583  chpub  26584  chebbnd1lem1  26833  chtppilimlem1  26837  rplogsumlem2  26849  perpneq  27698  ragperp  27701  tocyc01  32009  cyc3evpm  32041  cycpmconjslem2  32046  cyc3conja  32048  ressdeg1  32315  lbsdiflsp0  32361  irngss  32401  esum2d  32732  ispisys2  32792  sigapisys  32794  sigapildsyslem  32800  sigapildsys  32801  sseqf  33032  tgoldbachgt  33316  bnj1172  33653  mhpind  40798  ismnushort  42655  cnrefiisplem  44144  hoiqssbllem3  44939  smflimlem3  45088
  Copyright terms: Public domain W3C validator