Theorem elin2d 4151

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906

This theorem is used by:  f1opwfi  9338  elfiun  9415  ordtypelem3  9507  infpwfien  10134  ttukeylem6  10585  fpwwe2lem11  10719  explecnv  16027  bitsinv1  16605  smuval2  16645  firest  17596  sscres  17991  funcres2c  18071  coffth  18106  rescfth  18107  catcoppccl  18285  catcfuccl  18286  catcxpccl  18374  psssdm2  18748  sylow2a  19826  frgpnabllem2  20081  idomdomd  20970  sralmod  21455  2idlridld  21541  ssdifidlprm  21635  zringlpirlem3  21763  mplind  22372  neiptoptop  23442  restbas  23469  ordtrest  23513  subbascn  23565  lmss  23609  cnconn  23733  clsconn  23741  conncompclo  23746  subislly  23793  cldllycmp  23807  1stckgenlem  23865  txcls  23916  txcnp  23932  txtube  23952  txcmplem1  23953  txkgen  23964  xkopt  23967  xkococnlem  23971  txconn  24001  basqtop  24023  tgqtop  24024  kqnrmlem1  24055  kqnrmlem2  24056  nrmhmph  24106  uzrest  24209  alexsubALTlem3  24361  ptcmplem2  24365  tsmslem1  24441  tsmsxplem1  24465  tsmsxplem2  24466  tsmsxp  24467  blin2  24741  met2ndci  24834  zdis  25129  reconnlem2  25140  reconn  25141  xrge0gsumle  25146  cnheibor  25269  lebnum  25278  nmoleub2lem3  25429  nmoleub3  25433  caussi  25611  minveclem4b  25745  minveclem4  25746  ovolfcl  25780  ovolfioo  25781  ovolficc  25782  ovolficcss  25783  ovolfsval  25784  ovoliunlem1  25816  ovolicc2lem4  25834  ovolicc2lem5  25835  uniiccdif  25892  uniioovol  25893  uniiccvol  25894  uniioombllem2a  25896  uniioombllem3a  25898  uniioombllem4  25900  uniioombllem5  25901  uniioombllem6  25902  vitalilem2  25923  vitalilem4  25925  ig1peu  26486  taylfvallem1  26677  tayl0  26682  ppisval  27424  chtf  27428  efchtcl  27431  chtge0  27432  ppinprm  27472  chtprm  27473  chtnprm  27474  chtwordi  27476  chtdif  27478  efchtdvds  27479  chtlepsi  27526  chtleppi  27530  pclogsum  27535  chpval2  27538  chpchtsum  27539  chpub  27540  chebbnd1lem1  27789  chtppilimlem1  27793  rplogsumlem2  27805  tglnpt4  29116  perpneq  29182  ragperp  29185  lnincplng  29255  angmgmaddeu1  29372  perpprlng  29421  prlngplngtr  29430  quadcgrprlng  29437  tocyc01  33672  cyc3evpm  33704  cycpmconjslem2  33709  cyc3conja  33711  mxidlirred  33990  dflringlem3  34021  dflring4  34023  pidufd  34068  1arithufdlem4  34072  ressdeg1  34091  exsslsb  34222  lbsdiflsp0  34251  irngss  34312  rtelextdg2lem  34351  esum2d  34718  ispisys2  34779  sigapisys  34781  sigapildsyslem  34787  sigapildsys  34788  sseqf  35017  tgoldbachgt  35285  bnj1172  35624  weiunfrlem  37232  dfttc4  37298  mhpind  43602  ismnushort  45270  cnrefiisplem  46808  hoiqssbllem3  47603  sssmf  47717  smflimlem3  47752  tmachlem-finscan  47914  tmachlem-exagreecover  47925  iinfconstbas  50143  ffthoppf  50242  fucoppc  50487  termcterm  50590  termcterm2  50591