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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  ordtypelem3  9493  ordtypelem4  9494  ordtypelem7  9497  infpwfien  10066  ttukeylem6  10517  fpwwe2lem11  10651  explecnv  15955  smuval2  16573  submrc  17717  coffth  18028  catcbascl  18202  acsfiindd  18642  frgpnabllem2  20002  ablfac2  20219  idomcringd  20889  2idllidld  21457  ssdifidlprm  21550  zringlpirlem2  21677  mplind  22287  neiptoptop  23357  restbas  23384  subbascn  23480  cnconn  23648  clsconn  23656  conncompclo  23661  cldllycmp  23722  llycmpkgen2  23777  1stckgenlem  23780  txcls  23831  txcnp  23847  ptcnplem  23848  xkopt  23882  txconn  23916  basqtop  23938  tgqtop  23939  kqnrmlem1  23970  kqnrmlem2  23971  nrmhmph  24021  ptcmplem5  24283  restutop  24464  blin2  24656  met2ndci  24749  zdis  25044  reconnlem2  25055  cnheibor  25184  lebnum  25193  nmoleub2lem  25343  nmoleub2lem3  25344  nmoleub2lem2  25345  nmoleub3  25348  nmhmcn  25349  minveclem4  25661  ovolicc2lem5  25750  ioorcl  25806  ig1peu  26401  taylfvallem1  26594  tayl0  26599  ppisval  27341  ppinprm  27389  chtnprm  27391  chtleppi  27447  pclogsum  27452  chpchtsum  27456  chpub  27457  chebbnd1lem1  27706  chtppilimlem1  27710  rplogsum  27764  tglnpt4  29003  perpcom  29068  perpneq  29069  ragperp  29072  lnincplng  29142  angmgmaddeu1  29259  perpprlng  29308  prlngplngtr  29317  quadcgrprlng  29324  tocyc01  33559  cyc3evpm  33591  cycpmgcl  33594  cycpmconjslem2  33596  cyc3conja  33598  mxidlirred  33876  dflringlem3  33907  dflring4  33909  rprmirredb  33943  pidufd  33954  1arithufdlem4  33958  exsslsb  34108  lbsdiflsp0  34137  esum2d  34604  ispisys2  34665  sigapisys  34667  sigapildsyslem  34673  sigapildsys  34674  eulerpartlemgvv  34888  tgoldbachgt  35172  weiunfrlem  37084  weiunfr  37087  dfttc4  37150  fvineqsneq  38167  pibt2  38172  limclner  46480  fourierdlem49  46984  tmachlem-agreeprod  47766  tmachlem-exagreecover  47775  iinfconstbas  49993  ffthoppf  50092  thincciso  50380  termcterm2  50441  termcciso  50443  termccisoeu  50444  termfucterm  50471  uobeqterm  50473