Theorem elin2d 4154

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905

This theorem is referenced by:  f1opwfi  9251  elfiun  9325  ordtypelem3  9417  infpwfien  9964  ttukeylem6  10416  fpwwe2lem11  10543  explecnv  15779  bitsinv1  16360  smuval2  16400  firest  17343  sscres  17738  funcres2c  17818  coffth  17853  rescfth  17854  catcoppccl  18032  catcfuccl  18033  catcxpccl  18121  psssdm2  18495  sylow2a  19539  frgpnabllem2  19794  idomdomd  20650  sralmod  21130  2idlridld  21201  zringlpirlem3  21410  mplind  22016  neiptoptop  23066  restbas  23093  ordtrest  23137  subbascn  23189  lmss  23233  cnconn  23357  clsconn  23365  conncompclo  23370  subislly  23416  cldllycmp  23430  1stckgenlem  23488  txcls  23539  txcnp  23555  txtube  23575  txcmplem1  23576  txkgen  23587  xkopt  23590  xkococnlem  23594  txconn  23624  basqtop  23646  tgqtop  23647  kqnrmlem1  23678  kqnrmlem2  23679  nrmhmph  23729  uzrest  23832  alexsubALTlem3  23984  ptcmplem2  23988  tsmslem1  24064  tsmsxplem1  24088  tsmsxplem2  24089  tsmsxp  24090  blin2  24364  met2ndci  24457  zdis  24752  reconnlem2  24763  reconn  24764  xrge0gsumle  24769  cnheibor  24901  lebnum  24910  nmoleub2lem3  25062  nmoleub3  25066  caussi  25244  minveclem4b  25378  minveclem4  25379  ovolfcl  25414  ovolfioo  25415  ovolficc  25416  ovolficcss  25417  ovolfsval  25418  ovoliunlem1  25450  ovolicc2lem4  25468  ovolicc2lem5  25469  uniiccdif  25526  uniioovol  25527  uniiccvol  25528  uniioombllem2a  25530  uniioombllem3a  25532  uniioombllem4  25534  uniioombllem5  25535  uniioombllem6  25536  vitalilem2  25557  vitalilem4  25559  ig1peu  26127  taylfvallem1  26311  tayl0  26316  ppisval  27061  chtf  27065  efchtcl  27068  chtge0  27069  ppinprm  27109  chtprm  27110  chtnprm  27111  chtwordi  27113  chtdif  27115  efchtdvds  27116  chtlepsi  27164  chtleppi  27168  pclogsum  27173  chpval2  27176  chpchtsum  27177  chpub  27178  chebbnd1lem1  27427  chtppilimlem1  27431  rplogsumlem2  27443  perpneq  28712  ragperp  28715  tocyc01  33128  cyc3evpm  33160  cycpmconjslem2  33165  cyc3conja  33167  ssdifidlprm  33467  mxidlirred  33481  pidufd  33552  1arithufdlem4  33556  ressdeg1  33575  exsslsb  33681  lbsdiflsp0  33711  irngss  33772  rtelextdg2lem  33811  esum2d  34178  ispisys2  34238  sigapisys  34240  sigapildsyslem  34246  sigapildsys  34247  sseqf  34477  tgoldbachgt  34748  bnj1172  35085  weiunfrlem  36580  mhpind  42752  ismnushort  44458  cnrefiisplem  45989  hoiqssbllem3  46784  smflimlem3  46933  iinfconstbas  49227  ffthoppf  49326  fucoppc  49571  termcterm  49674  termcterm2  49675