Theorem elin2d 4199

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

Syntax hints:   → wi 4   ∈ wcel 2105   ∩ cin 3947

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955

This theorem is referenced by:  f1opwfi  9362  elfiun  9431  ordtypelem3  9521  infpwfien  10063  ttukeylem6  10515  fpwwe2lem11  10642  explecnv  15818  bitsinv1  16390  smuval2  16430  firest  17385  sscres  17777  funcres2c  17861  coffth  17896  rescfth  17897  catcoppccl  18077  catcoppcclOLD  18078  catcfuccl  18079  catcfucclOLD  18080  catcxpccl  18169  catcxpcclOLD  18170  psssdm2  18544  sylow2a  19535  frgpnabllem2  19790  sralmod  21043  2idlridld  21105  zringlpirlem3  21324  mplind  21942  neiptoptop  22955  restbas  22982  ordtrest  23026  subbascn  23078  lmss  23122  cnconn  23246  clsconn  23254  conncompclo  23259  subislly  23305  cldllycmp  23319  1stckgenlem  23377  txcls  23428  txcnp  23444  txtube  23464  txcmplem1  23465  txkgen  23476  xkopt  23479  xkococnlem  23483  txconn  23513  basqtop  23535  tgqtop  23536  kqnrmlem1  23567  kqnrmlem2  23568  nrmhmph  23618  uzrest  23721  alexsubALTlem3  23873  ptcmplem2  23877  tsmslem1  23953  tsmsxplem1  23977  tsmsxplem2  23978  tsmsxp  23979  blin2  24255  met2ndci  24351  zdis  24652  reconnlem2  24663  reconn  24664  xrge0gsumle  24669  cnheibor  24801  lebnum  24810  nmoleub2lem3  24962  nmoleub3  24966  caussi  25145  minveclem4b  25279  minveclem4  25280  ovolfcl  25315  ovolfioo  25316  ovolficc  25317  ovolficcss  25318  ovolfsval  25319  ovoliunlem1  25351  ovolicc2lem4  25369  ovolicc2lem5  25370  uniiccdif  25427  uniioovol  25428  uniiccvol  25429  uniioombllem2a  25431  uniioombllem3a  25433  uniioombllem4  25435  uniioombllem5  25436  uniioombllem6  25437  vitalilem2  25458  vitalilem4  25460  ig1peu  26027  taylfvallem1  26208  tayl0  26213  ppisval  26949  chtf  26953  efchtcl  26956  chtge0  26957  ppinprm  26997  chtprm  26998  chtnprm  26999  chtwordi  27001  chtdif  27003  efchtdvds  27004  chtlepsi  27052  chtleppi  27056  pclogsum  27061  chpval2  27064  chpchtsum  27065  chpub  27066  chebbnd1lem1  27315  chtppilimlem1  27319  rplogsumlem2  27331  perpneq  28398  ragperp  28401  tocyc01  32713  cyc3evpm  32745  cycpmconjslem2  32750  cyc3conja  32752  idomdomd  32810  mxidlirred  33028  ressdeg1  33091  lbsdiflsp0  33165  irngss  33206  esum2d  33555  ispisys2  33615  sigapisys  33617  sigapildsyslem  33623  sigapildsys  33624  sseqf  33855  tgoldbachgt  34139  bnj1172  34476  mhpind  41629  ismnushort  43523  cnrefiisplem  45004  hoiqssbllem3  45799  smflimlem3  45948