Theorem elin2d 4158

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 4155	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝑋 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  f1opwfi  9309  elfiun  9386  ordtypelem3  9478  infpwfien  10042  ttukeylem6  10493  fpwwe2lem11  10621  explecnv  15915  bitsinv1  16495  smuval2  16535  firest  17480  sscres  17875  funcres2c  17955  coffth  17990  rescfth  17991  catcoppccl  18169  catcfuccl  18170  catcxpccl  18258  psssdm2  18632  sylow2a  19684  frgpnabllem2  19939  idomdomd  20824  sralmod  21308  2idlridld  21394  ssdifidlprm  21486  zringlpirlem3  21614  mplind  22221  neiptoptop  23288  restbas  23315  ordtrest  23359  subbascn  23411  lmss  23455  cnconn  23579  clsconn  23587  conncompclo  23592  subislly  23638  cldllycmp  23652  1stckgenlem  23710  txcls  23761  txcnp  23777  txtube  23797  txcmplem1  23798  txkgen  23809  xkopt  23812  xkococnlem  23816  txconn  23846  basqtop  23868  tgqtop  23869  kqnrmlem1  23900  kqnrmlem2  23901  nrmhmph  23951  uzrest  24054  alexsubALTlem3  24206  ptcmplem2  24210  tsmslem1  24286  tsmsxplem1  24310  tsmsxplem2  24311  tsmsxp  24312  blin2  24586  met2ndci  24679  zdis  24974  reconnlem2  24985  reconn  24986  xrge0gsumle  24991  cnheibor  25114  lebnum  25123  nmoleub2lem3  25274  nmoleub3  25278  caussi  25456  minveclem4b  25590  minveclem4  25591  ovolfcl  25625  ovolfioo  25626  ovolficc  25627  ovolficcss  25628  ovolfsval  25629  ovoliunlem1  25661  ovolicc2lem4  25679  ovolicc2lem5  25680  uniiccdif  25737  uniioovol  25738  uniiccvol  25739  uniioombllem2a  25741  uniioombllem3a  25743  uniioombllem4  25745  uniioombllem5  25746  uniioombllem6  25747  vitalilem2  25768  vitalilem4  25770  ig1peu  26332  taylfvallem1  26520  tayl0  26525  ppisval  27268  chtf  27272  efchtcl  27275  chtge0  27276  ppinprm  27316  chtprm  27317  chtnprm  27318  chtwordi  27320  chtdif  27322  efchtdvds  27323  chtlepsi  27370  chtleppi  27374  pclogsum  27379  chpval2  27382  chpchtsum  27383  chpub  27384  chebbnd1lem1  27633  chtppilimlem1  27637  rplogsumlem2  27649  tglnpt4  28928  perpneq  28994  ragperp  28997  lnincplng  29066  perpprlng  29200  prlngplngtr  29209  quadcgrprlng  29216  tocyc01  33438  cyc3evpm  33470  cycpmconjslem2  33475  cyc3conja  33477  mxidlirred  33755  dflringlem3  33786  dflring4  33788  pidufd  33833  1arithufdlem4  33837  ressdeg1  33856  exsslsb  33987  lbsdiflsp0  34016  irngss  34077  rtelextdg2lem  34116  esum2d  34483  ispisys2  34543  sigapisys  34545  sigapildsyslem  34551  sigapildsys  34552  sseqf  34782  tgoldbachgt  35050  bnj1172  35389  weiunfrlem  36975  dfttc4  37041  mhpind  43326  ismnushort  45011  cnrefiisplem  46543  hoiqssbllem3  47338  sssmf  47452  smflimlem3  47487  iinfconstbas  49844  ffthoppf  49943  fucoppc  50188  termcterm  50291  termcterm2  50292