Theorem elin2d 4200

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3948

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956

This theorem is referenced by:  f1opwfi  9356  elfiun  9425  ordtypelem3  9515  infpwfien  10057  ttukeylem6  10509  fpwwe2lem11  10636  explecnv  15811  bitsinv1  16383  smuval2  16423  firest  17378  sscres  17770  funcres2c  17852  coffth  17887  rescfth  17888  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  psssdm2  18534  sylow2a  19487  frgpnabllem2  19742  sralmod  20809  2idlridld  20867  zringlpirlem3  21034  mplind  21631  neiptoptop  22635  restbas  22662  ordtrest  22706  subbascn  22758  lmss  22802  cnconn  22926  clsconn  22934  conncompclo  22939  subislly  22985  cldllycmp  22999  1stckgenlem  23057  txcls  23108  txcnp  23124  txtube  23144  txcmplem1  23145  txkgen  23156  xkopt  23159  xkococnlem  23163  txconn  23193  basqtop  23215  tgqtop  23216  kqnrmlem1  23247  kqnrmlem2  23248  nrmhmph  23298  uzrest  23401  alexsubALTlem3  23553  ptcmplem2  23557  tsmslem1  23633  tsmsxplem1  23657  tsmsxplem2  23658  tsmsxp  23659  blin2  23935  met2ndci  24031  zdis  24332  reconnlem2  24343  reconn  24344  xrge0gsumle  24349  cnheibor  24471  lebnum  24480  nmoleub2lem3  24631  nmoleub3  24635  caussi  24814  minveclem4b  24948  minveclem4  24949  ovolfcl  24983  ovolfioo  24984  ovolficc  24985  ovolficcss  24986  ovolfsval  24987  ovoliunlem1  25019  ovolicc2lem4  25037  ovolicc2lem5  25038  uniiccdif  25095  uniioovol  25096  uniiccvol  25097  uniioombllem2a  25099  uniioombllem3a  25101  uniioombllem4  25103  uniioombllem5  25104  uniioombllem6  25105  vitalilem2  25126  vitalilem4  25128  ig1peu  25689  taylfvallem1  25869  tayl0  25874  ppisval  26608  chtf  26612  efchtcl  26615  chtge0  26616  ppinprm  26656  chtprm  26657  chtnprm  26658  chtwordi  26660  chtdif  26662  efchtdvds  26663  chtlepsi  26709  chtleppi  26713  pclogsum  26718  chpval2  26721  chpchtsum  26722  chpub  26723  chebbnd1lem1  26972  chtppilimlem1  26976  rplogsumlem2  26988  perpneq  27965  ragperp  27968  tocyc01  32277  cyc3evpm  32309  cycpmconjslem2  32314  cyc3conja  32316  idomdomd  32374  mxidlirred  32588  ressdeg1  32651  lbsdiflsp0  32711  irngss  32751  esum2d  33091  ispisys2  33151  sigapisys  33153  sigapildsyslem  33159  sigapildsys  33160  sseqf  33391  tgoldbachgt  33675  bnj1172  34012  mhpind  41166  ismnushort  43060  cnrefiisplem  44545  hoiqssbllem3  45340  smflimlem3  45489