Theorem elin2d 4150

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 4147	. 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  9235  elfiun  9309  ordtypelem3  9401  infpwfien  9948  ttukeylem6  10400  fpwwe2lem11  10527  explecnv  15767  bitsinv1  16348  smuval2  16388  firest  17331  sscres  17725  funcres2c  17805  coffth  17840  rescfth  17841  catcoppccl  18019  catcfuccl  18020  catcxpccl  18108  psssdm2  18482  sylow2a  19526  frgpnabllem2  19781  idomdomd  20636  sralmod  21116  2idlridld  21187  zringlpirlem3  21396  mplind  22000  neiptoptop  23041  restbas  23068  ordtrest  23112  subbascn  23164  lmss  23208  cnconn  23332  clsconn  23340  conncompclo  23345  subislly  23391  cldllycmp  23405  1stckgenlem  23463  txcls  23514  txcnp  23530  txtube  23550  txcmplem1  23551  txkgen  23562  xkopt  23565  xkococnlem  23569  txconn  23599  basqtop  23621  tgqtop  23622  kqnrmlem1  23653  kqnrmlem2  23654  nrmhmph  23704  uzrest  23807  alexsubALTlem3  23959  ptcmplem2  23963  tsmslem1  24039  tsmsxplem1  24063  tsmsxplem2  24064  tsmsxp  24065  blin2  24339  met2ndci  24432  zdis  24727  reconnlem2  24738  reconn  24739  xrge0gsumle  24744  cnheibor  24876  lebnum  24885  nmoleub2lem3  25037  nmoleub3  25041  caussi  25219  minveclem4b  25353  minveclem4  25354  ovolfcl  25389  ovolfioo  25390  ovolficc  25391  ovolficcss  25392  ovolfsval  25393  ovoliunlem1  25425  ovolicc2lem4  25443  ovolicc2lem5  25444  uniiccdif  25501  uniioovol  25502  uniiccvol  25503  uniioombllem2a  25505  uniioombllem3a  25507  uniioombllem4  25509  uniioombllem5  25510  uniioombllem6  25511  vitalilem2  25532  vitalilem4  25534  ig1peu  26102  taylfvallem1  26286  tayl0  26291  ppisval  27036  chtf  27040  efchtcl  27043  chtge0  27044  ppinprm  27084  chtprm  27085  chtnprm  27086  chtwordi  27088  chtdif  27090  efchtdvds  27091  chtlepsi  27139  chtleppi  27143  pclogsum  27148  chpval2  27151  chpchtsum  27152  chpub  27153  chebbnd1lem1  27402  chtppilimlem1  27406  rplogsumlem2  27418  perpneq  28687  ragperp  28690  tocyc01  33079  cyc3evpm  33111  cycpmconjslem2  33116  cyc3conja  33118  ssdifidlprm  33415  mxidlirred  33429  pidufd  33500  1arithufdlem4  33504  ressdeg1  33521  exsslsb  33601  lbsdiflsp0  33631  irngss  33692  rtelextdg2lem  33731  esum2d  34098  ispisys2  34158  sigapisys  34160  sigapildsyslem  34166  sigapildsys  34167  sseqf  34397  tgoldbachgt  34668  bnj1172  35005  weiunfrlem  36498  mhpind  42627  ismnushort  44334  cnrefiisplem  45867  hoiqssbllem3  46662  smflimlem3  46811  iinfconstbas  49098  ffthoppf  49197  fucoppc  49442  termcterm  49545  termcterm2  49546