Theorem elin2d 4145

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

Step	Hyp	Ref	Expression
1		elin1d.1	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
2		elinel2 4142	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  f1opwfi  9266  elfiun  9343  ordtypelem3  9435  infpwfien  9984  ttukeylem6  10436  fpwwe2lem11  10564  explecnv  15830  bitsinv1  16411  smuval2  16451  firest  17395  sscres  17790  funcres2c  17870  coffth  17905  rescfth  17906  catcoppccl  18084  catcfuccl  18085  catcxpccl  18173  psssdm2  18547  sylow2a  19594  frgpnabllem2  19849  idomdomd  20703  sralmod  21182  2idlridld  21253  zringlpirlem3  21444  mplind  22048  neiptoptop  23096  restbas  23123  ordtrest  23167  subbascn  23219  lmss  23263  cnconn  23387  clsconn  23395  conncompclo  23400  subislly  23446  cldllycmp  23460  1stckgenlem  23518  txcls  23569  txcnp  23585  txtube  23605  txcmplem1  23606  txkgen  23617  xkopt  23620  xkococnlem  23624  txconn  23654  basqtop  23676  tgqtop  23677  kqnrmlem1  23708  kqnrmlem2  23709  nrmhmph  23759  uzrest  23862  alexsubALTlem3  24014  ptcmplem2  24018  tsmslem1  24094  tsmsxplem1  24118  tsmsxplem2  24119  tsmsxp  24120  blin2  24394  met2ndci  24487  zdis  24782  reconnlem2  24793  reconn  24794  xrge0gsumle  24799  cnheibor  24922  lebnum  24931  nmoleub2lem3  25082  nmoleub3  25086  caussi  25264  minveclem4b  25398  minveclem4  25399  ovolfcl  25433  ovolfioo  25434  ovolficc  25435  ovolficcss  25436  ovolfsval  25437  ovoliunlem1  25469  ovolicc2lem4  25487  ovolicc2lem5  25488  uniiccdif  25545  uniioovol  25546  uniiccvol  25547  uniioombllem2a  25549  uniioombllem3a  25551  uniioombllem4  25553  uniioombllem5  25554  uniioombllem6  25555  vitalilem2  25576  vitalilem4  25578  ig1peu  26140  taylfvallem1  26322  tayl0  26327  ppisval  27067  chtf  27071  efchtcl  27074  chtge0  27075  ppinprm  27115  chtprm  27116  chtnprm  27117  chtwordi  27119  chtdif  27121  efchtdvds  27122  chtlepsi  27169  chtleppi  27173  pclogsum  27178  chpval2  27181  chpchtsum  27182  chpub  27183  chebbnd1lem1  27432  chtppilimlem1  27436  rplogsumlem2  27448  perpneq  28782  ragperp  28785  tocyc01  33179  cyc3evpm  33211  cycpmconjslem2  33216  cyc3conja  33218  ssdifidlprm  33518  mxidlirred  33532  pidufd  33603  1arithufdlem4  33607  ressdeg1  33626  exsslsb  33741  lbsdiflsp0  33770  irngss  33831  rtelextdg2lem  33870  esum2d  34237  ispisys2  34297  sigapisys  34299  sigapildsyslem  34305  sigapildsys  34306  sseqf  34536  tgoldbachgt  34807  bnj1172  35143  weiunfrlem  36646  dfttc4  36712  mhpind  43027  ismnushort  44728  cnrefiisplem  46257  hoiqssbllem3  47052  smflimlem3  47201  iinfconstbas  49541  ffthoppf  49640  fucoppc  49885  termcterm  49988  termcterm2  49989