Theorem elin1d 4213

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

Syntax hints:   → wi 4   ∈ wcel 2105   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969

This theorem is referenced by:  ordtypelem3  9557  ordtypelem4  9558  ordtypelem7  9561  infpwfien  10099  ttukeylem6  10551  fpwwe2lem11  10678  explecnv  15897  smuval2  16515  submrc  17672  coffth  17989  catcbascl  18165  catcoppcclOLD  18171  catcfucclOLD  18173  catcxpcclOLD  18263  acsfiindd  18610  frgpnabllem2  19906  ablfac2  20123  idomcringd  20743  2idllidld  21281  zringlpirlem2  21491  mplind  22111  neiptoptop  23154  restbas  23181  subbascn  23277  cnconn  23445  clsconn  23453  conncompclo  23458  cldllycmp  23518  llycmpkgen2  23573  1stckgenlem  23576  txcls  23627  txcnp  23643  ptcnplem  23644  xkopt  23678  txconn  23712  basqtop  23734  tgqtop  23735  kqnrmlem1  23766  kqnrmlem2  23767  nrmhmph  23817  ptcmplem5  24079  restutop  24261  blin2  24454  met2ndci  24550  zdis  24851  reconnlem2  24862  cnheibor  25000  lebnum  25009  nmoleub2lem  25160  nmoleub2lem3  25161  nmoleub2lem2  25162  nmoleub3  25165  nmhmcn  25166  minveclem4  25479  ovolicc2lem5  25569  ioorcl  25625  ig1peu  26228  taylfvallem1  26412  tayl0  26417  ppisval  27161  ppinprm  27209  chtnprm  27211  chtleppi  27268  pclogsum  27273  chpchtsum  27277  chpub  27278  chebbnd1lem1  27527  chtppilimlem1  27531  rplogsum  27585  perpcom  28735  perpneq  28736  ragperp  28739  tocyc01  33120  cyc3evpm  33152  cycpmgcl  33155  cycpmconjslem2  33157  cyc3conja  33159  idomrcanOLD  33265  unitpidl1  33431  ssdifidlprm  33465  mxidlirredi  33478  mxidlirred  33479  rprmirredb  33539  pidufd  33550  1arithufdlem4  33554  lbsdiflsp0  33653  esum2d  34073  ispisys2  34133  sigapisys  34135  sigapildsyslem  34141  sigapildsys  34142  eulerpartlemgvv  34357  tgoldbachgt  34656  weiunfrlem  36446  weiunfr  36449  fvineqsneq  37394  pibt2  37399  limclner  45606  thincciso  48848