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 2111   ∩ cin 3896

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  f1opwfi  9246  elfiun  9320  ordtypelem3  9412  infpwfien  9959  ttukeylem6  10411  fpwwe2lem11  10538  explecnv  15778  bitsinv1  16359  smuval2  16399  firest  17342  sscres  17736  funcres2c  17816  coffth  17851  rescfth  17852  catcoppccl  18030  catcfuccl  18031  catcxpccl  18119  psssdm2  18493  sylow2a  19537  frgpnabllem2  19792  idomdomd  20647  sralmod  21127  2idlridld  21198  zringlpirlem3  21407  mplind  22011  neiptoptop  23052  restbas  23079  ordtrest  23123  subbascn  23175  lmss  23219  cnconn  23343  clsconn  23351  conncompclo  23356  subislly  23402  cldllycmp  23416  1stckgenlem  23474  txcls  23525  txcnp  23541  txtube  23561  txcmplem1  23562  txkgen  23573  xkopt  23576  xkococnlem  23580  txconn  23610  basqtop  23632  tgqtop  23633  kqnrmlem1  23664  kqnrmlem2  23665  nrmhmph  23715  uzrest  23818  alexsubALTlem3  23970  ptcmplem2  23974  tsmslem1  24050  tsmsxplem1  24074  tsmsxplem2  24075  tsmsxp  24076  blin2  24350  met2ndci  24443  zdis  24738  reconnlem2  24749  reconn  24750  xrge0gsumle  24755  cnheibor  24887  lebnum  24896  nmoleub2lem3  25048  nmoleub3  25052  caussi  25230  minveclem4b  25364  minveclem4  25365  ovolfcl  25400  ovolfioo  25401  ovolficc  25402  ovolficcss  25403  ovolfsval  25404  ovoliunlem1  25436  ovolicc2lem4  25454  ovolicc2lem5  25455  uniiccdif  25512  uniioovol  25513  uniiccvol  25514  uniioombllem2a  25516  uniioombllem3a  25518  uniioombllem4  25520  uniioombllem5  25521  uniioombllem6  25522  vitalilem2  25543  vitalilem4  25545  ig1peu  26113  taylfvallem1  26297  tayl0  26302  ppisval  27047  chtf  27051  efchtcl  27054  chtge0  27055  ppinprm  27095  chtprm  27096  chtnprm  27097  chtwordi  27099  chtdif  27101  efchtdvds  27102  chtlepsi  27150  chtleppi  27154  pclogsum  27159  chpval2  27162  chpchtsum  27163  chpub  27164  chebbnd1lem1  27413  chtppilimlem1  27417  rplogsumlem2  27429  perpneq  28698  ragperp  28701  tocyc01  33094  cyc3evpm  33126  cycpmconjslem2  33131  cyc3conja  33133  ssdifidlprm  33430  mxidlirred  33444  pidufd  33515  1arithufdlem4  33519  ressdeg1  33536  exsslsb  33616  lbsdiflsp0  33646  irngss  33707  rtelextdg2lem  33746  esum2d  34113  ispisys2  34173  sigapisys  34175  sigapildsyslem  34181  sigapildsys  34182  sseqf  34412  tgoldbachgt  34683  bnj1172  35020  weiunfrlem  36515  mhpind  42693  ismnushort  44399  cnrefiisplem  45932  hoiqssbllem3  46727  smflimlem3  46876  iinfconstbas  49172  ffthoppf  49271  fucoppc  49516  termcterm  49619  termcterm2  49620