Theorem elin1d 4158

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910

This theorem is referenced by:  ordtypelem3  9437  ordtypelem4  9438  ordtypelem7  9441  infpwfien  9984  ttukeylem6  10436  fpwwe2lem11  10564  explecnv  15800  smuval2  16421  submrc  17563  coffth  17874  catcbascl  18048  acsfiindd  18488  frgpnabllem2  19815  ablfac2  20032  idomcringd  20672  2idllidld  21221  zringlpirlem2  21430  mplind  22037  neiptoptop  23087  restbas  23114  subbascn  23210  cnconn  23378  clsconn  23386  conncompclo  23391  cldllycmp  23451  llycmpkgen2  23506  1stckgenlem  23509  txcls  23560  txcnp  23576  ptcnplem  23577  xkopt  23611  txconn  23645  basqtop  23667  tgqtop  23668  kqnrmlem1  23699  kqnrmlem2  23700  nrmhmph  23750  ptcmplem5  24012  restutop  24193  blin2  24385  met2ndci  24478  zdis  24773  reconnlem2  24784  cnheibor  24922  lebnum  24931  nmoleub2lem  25082  nmoleub2lem3  25083  nmoleub2lem2  25084  nmoleub3  25087  nmhmcn  25088  minveclem4  25400  ovolicc2lem5  25490  ioorcl  25546  ig1peu  26148  taylfvallem1  26332  tayl0  26337  ppisval  27082  ppinprm  27130  chtnprm  27132  chtleppi  27189  pclogsum  27194  chpchtsum  27198  chpub  27199  chebbnd1lem1  27448  chtppilimlem1  27452  rplogsum  27506  perpcom  28797  perpneq  28798  ragperp  28801  tocyc01  33212  cyc3evpm  33244  cycpmgcl  33247  cycpmconjslem2  33249  cyc3conja  33251  idomrcanOLD  33376  unitpidl1  33517  ssdifidlprm  33551  mxidlirredi  33564  mxidlirred  33565  rprmirredb  33625  pidufd  33636  1arithufdlem4  33640  exsslsb  33774  lbsdiflsp0  33804  esum2d  34271  ispisys2  34331  sigapisys  34333  sigapildsyslem  34339  sigapildsys  34340  eulerpartlemgvv  34554  tgoldbachgt  34841  weiunfrlem  36680  weiunfr  36683  fvineqsneq  37667  pibt2  37672  limclner  46009  iinfconstbas  49425  ffthoppf  49524  thincciso  49812  termcterm2  49873  termcciso  49875  termccisoeu  49876  termfucterm  49903  uobeqterm  49905