Theorem elin1d 4157

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
elin1d	⊢ (𝜑 → 𝑋 ∈ 𝐴)

Proof of Theorem elin1d

Step	Hyp	Ref	Expression
1		elin1d.1	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
2		elinel1 4154	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝑋 ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  ordtypelem3  9478  ordtypelem4  9479  ordtypelem7  9482  infpwfien  10042  ttukeylem6  10493  fpwwe2lem11  10621  explecnv  15915  smuval2  16535  submrc  17679  coffth  17990  catcbascl  18164  acsfiindd  18604  frgpnabllem2  19939  ablfac2  20156  idomcringd  20825  2idllidld  21393  ssdifidlprm  21486  zringlpirlem2  21613  mplind  22221  neiptoptop  23288  restbas  23315  subbascn  23411  cnconn  23579  clsconn  23587  conncompclo  23592  cldllycmp  23652  llycmpkgen2  23707  1stckgenlem  23710  txcls  23761  txcnp  23777  ptcnplem  23778  xkopt  23812  txconn  23846  basqtop  23868  tgqtop  23869  kqnrmlem1  23900  kqnrmlem2  23901  nrmhmph  23951  ptcmplem5  24213  restutop  24394  blin2  24586  met2ndci  24679  zdis  24974  reconnlem2  24985  cnheibor  25114  lebnum  25123  nmoleub2lem  25273  nmoleub2lem3  25274  nmoleub2lem2  25275  nmoleub3  25278  nmhmcn  25279  minveclem4  25591  ovolicc2lem5  25680  ioorcl  25736  ig1peu  26332  taylfvallem1  26520  tayl0  26525  ppisval  27268  ppinprm  27316  chtnprm  27318  chtleppi  27374  pclogsum  27379  chpchtsum  27383  chpub  27384  chebbnd1lem1  27633  chtppilimlem1  27637  rplogsum  27691  tglnpt4  28928  perpcom  28993  perpneq  28994  ragperp  28997  lnincplng  29066  perpprlng  29200  prlngplngtr  29209  quadcgrprlng  29216  tocyc01  33438  cyc3evpm  33470  cycpmgcl  33473  cycpmconjslem2  33475  cyc3conja  33477  mxidlirred  33755  dflringlem3  33786  dflring4  33788  rprmirredb  33822  pidufd  33833  1arithufdlem4  33837  exsslsb  33987  lbsdiflsp0  34016  esum2d  34483  ispisys2  34543  sigapisys  34545  sigapildsyslem  34551  sigapildsys  34552  eulerpartlemgvv  34766  tgoldbachgt  35050  weiunfrlem  36975  weiunfr  36978  dfttc4  37041  fvineqsneq  38058  pibt2  38063  limclner  46365  fourierdlem49  46869  iinfconstbas  49844  ffthoppf  49943  thincciso  50231  termcterm2  50292  termcciso  50294  termccisoeu  50295  termfucterm  50322  uobeqterm  50324