Theorem elin1d 4204

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958

This theorem is referenced by:  ordtypelem3  9560  ordtypelem4  9561  ordtypelem7  9564  infpwfien  10102  ttukeylem6  10554  fpwwe2lem11  10681  explecnv  15901  smuval2  16519  submrc  17671  coffth  17983  catcbascl  18157  acsfiindd  18598  frgpnabllem2  19892  ablfac2  20109  idomcringd  20727  2idllidld  21264  zringlpirlem2  21474  mplind  22094  neiptoptop  23139  restbas  23166  subbascn  23262  cnconn  23430  clsconn  23438  conncompclo  23443  cldllycmp  23503  llycmpkgen2  23558  1stckgenlem  23561  txcls  23612  txcnp  23628  ptcnplem  23629  xkopt  23663  txconn  23697  basqtop  23719  tgqtop  23720  kqnrmlem1  23751  kqnrmlem2  23752  nrmhmph  23802  ptcmplem5  24064  restutop  24246  blin2  24439  met2ndci  24535  zdis  24838  reconnlem2  24849  cnheibor  24987  lebnum  24996  nmoleub2lem  25147  nmoleub2lem3  25148  nmoleub2lem2  25149  nmoleub3  25152  nmhmcn  25153  minveclem4  25466  ovolicc2lem5  25556  ioorcl  25612  ig1peu  26214  taylfvallem1  26398  tayl0  26403  ppisval  27147  ppinprm  27195  chtnprm  27197  chtleppi  27254  pclogsum  27259  chpchtsum  27263  chpub  27264  chebbnd1lem1  27513  chtppilimlem1  27517  rplogsum  27571  perpcom  28721  perpneq  28722  ragperp  28725  tocyc01  33138  cyc3evpm  33170  cycpmgcl  33173  cycpmconjslem2  33175  cyc3conja  33177  idomrcanOLD  33285  unitpidl1  33452  ssdifidlprm  33486  mxidlirredi  33499  mxidlirred  33500  rprmirredb  33560  pidufd  33571  1arithufdlem4  33575  exsslsb  33647  lbsdiflsp0  33677  esum2d  34094  ispisys2  34154  sigapisys  34156  sigapildsyslem  34162  sigapildsys  34163  eulerpartlemgvv  34378  tgoldbachgt  34678  weiunfrlem  36465  weiunfr  36468  fvineqsneq  37413  pibt2  37418  limclner  45666  thincciso  49102  termcterm2  49146