Theorem elin2d 4133

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894

This theorem is referenced by:  f1opwfi  9123  elfiun  9189  ordtypelem3  9279  infpwfien  9818  ttukeylem6  10270  fpwwe2lem11  10397  explecnv  15577  bitsinv1  16149  smuval2  16189  firest  17143  sscres  17535  funcres2c  17617  coffth  17652  rescfth  17653  catcoppccl  17832  catcoppcclOLD  17833  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  psssdm2  18299  sylow2a  19224  frgpnabllem2  19475  sralmod  20457  zringlpirlem3  20686  mplind  21278  neiptoptop  22282  restbas  22309  ordtrest  22353  subbascn  22405  lmss  22449  cnconn  22573  clsconn  22581  conncompclo  22586  subislly  22632  cldllycmp  22646  1stckgenlem  22704  txcls  22755  txcnp  22771  txtube  22791  txcmplem1  22792  txkgen  22803  xkopt  22806  xkococnlem  22810  txconn  22840  basqtop  22862  tgqtop  22863  kqnrmlem1  22894  kqnrmlem2  22895  nrmhmph  22945  uzrest  23048  alexsubALTlem3  23200  ptcmplem2  23204  tsmslem1  23280  tsmsxplem1  23304  tsmsxplem2  23305  tsmsxp  23306  blin2  23582  met2ndci  23678  zdis  23979  reconnlem2  23990  reconn  23991  xrge0gsumle  23996  cnheibor  24118  lebnum  24127  nmoleub2lem3  24278  nmoleub3  24282  caussi  24461  minveclem4b  24595  minveclem4  24596  ovolfcl  24630  ovolfioo  24631  ovolficc  24632  ovolficcss  24633  ovolfsval  24634  ovoliunlem1  24666  ovolicc2lem4  24684  ovolicc2lem5  24685  uniiccdif  24742  uniioovol  24743  uniiccvol  24744  uniioombllem2a  24746  uniioombllem3a  24748  uniioombllem4  24750  uniioombllem5  24751  uniioombllem6  24752  vitalilem2  24773  vitalilem4  24775  ig1peu  25336  taylfvallem1  25516  tayl0  25521  ppisval  26253  chtf  26257  efchtcl  26260  chtge0  26261  ppinprm  26301  chtprm  26302  chtnprm  26303  chtwordi  26305  chtdif  26307  efchtdvds  26308  chtlepsi  26354  chtleppi  26358  pclogsum  26363  chpval2  26366  chpchtsum  26367  chpub  26368  chebbnd1lem1  26617  chtppilimlem1  26621  rplogsumlem2  26633  perpneq  27075  ragperp  27078  tocyc01  31385  cyc3evpm  31417  cycpmconjslem2  31422  cyc3conja  31424  lbsdiflsp0  31707  esum2d  32061  ispisys2  32121  sigapisys  32123  sigapildsyslem  32129  sigapildsys  32130  sseqf  32359  tgoldbachgt  32643  bnj1172  32981  mhpind  40283  ismnushort  41919  cnrefiisplem  43370  hoiqssbllem3  44162  smflimlem3  44308