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

Proof of Theorem elin1d

Step	Hyp	Ref	Expression
1		elin1d.1	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
2		elinel1 4147	. 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:  ordtypelem3  9514  ordtypelem4  9515  ordtypelem7  9518  infpwfien  10141  ttukeylem6  10592  fpwwe2lem11  10726  explecnv  16034  smuval2  16652  submrc  17802  coffth  18113  catcbascl  18287  acsfiindd  18727  frgpnabllem2  20088  ablfac2  20305  idomcringd  20978  2idllidld  21547  ssdifidlprm  21642  zringlpirlem2  21769  mplind  22379  neiptoptop  23449  restbas  23476  subbascn  23572  cnconn  23740  clsconn  23748  conncompclo  23753  cldllycmp  23814  llycmpkgen2  23869  1stckgenlem  23872  txcls  23923  txcnp  23939  ptcnplem  23940  xkopt  23974  txconn  24008  basqtop  24030  tgqtop  24031  kqnrmlem1  24062  kqnrmlem2  24063  nrmhmph  24113  ptcmplem5  24375  restutop  24556  blin2  24748  met2ndci  24841  zdis  25136  reconnlem2  25147  cnheibor  25276  lebnum  25285  nmoleub2lem  25435  nmoleub2lem3  25436  nmoleub2lem2  25437  nmoleub3  25440  nmhmcn  25441  minveclem4  25753  ovolicc2lem5  25842  ioorcl  25898  ig1peu  26493  taylfvallem1  26684  tayl0  26689  ppisval  27431  ppinprm  27479  chtnprm  27481  chtleppi  27537  pclogsum  27542  chpchtsum  27546  chpub  27547  chebbnd1lem1  27796  chtppilimlem1  27800  rplogsum  27854  tglnpt4  29123  perpcom  29188  perpneq  29189  ragperp  29192  lnincplng  29262  angmgmaddeu1  29379  perpprlng  29428  prlngplngtr  29437  quadcgrprlng  29444  tocyc01  33679  cyc3evpm  33711  cycpmgcl  33714  cycpmconjslem2  33716  cyc3conja  33718  mxidlirred  33997  dflringlem3  34028  dflring4  34030  rprmirredb  34064  pidufd  34075  1arithufdlem4  34079  exsslsb  34229  lbsdiflsp0  34258  esum2d  34725  ispisys2  34786  sigapisys  34788  sigapildsyslem  34794  sigapildsys  34795  eulerpartlemgvv  35008  tgoldbachgt  35292  weiunfrlem  37252  weiunfr  37255  dfttc4  37318  fvineqsneq  38335  pibt2  38340  limclner  46660  fourierdlem49  47164  tmachlem-agreeprod  47946  tmachlem-exagreecover  47955  iinfconstbas  50173  ffthoppf  50272  thincciso  50560  termcterm2  50621  termcciso  50623  termccisoeu  50624  termfucterm  50651  uobeqterm  50653