Theorem elin1d 4163

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3910

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918

This theorem is referenced by:  ordtypelem3  9449  ordtypelem4  9450  ordtypelem7  9453  infpwfien  9991  ttukeylem6  10443  fpwwe2lem11  10570  explecnv  15807  smuval2  16428  submrc  17569  coffth  17880  catcbascl  18054  acsfiindd  18494  frgpnabllem2  19788  ablfac2  20005  idomcringd  20647  2idllidld  21196  zringlpirlem2  21405  mplind  22010  neiptoptop  23051  restbas  23078  subbascn  23174  cnconn  23342  clsconn  23350  conncompclo  23355  cldllycmp  23415  llycmpkgen2  23470  1stckgenlem  23473  txcls  23524  txcnp  23540  ptcnplem  23541  xkopt  23575  txconn  23609  basqtop  23631  tgqtop  23632  kqnrmlem1  23663  kqnrmlem2  23664  nrmhmph  23714  ptcmplem5  23976  restutop  24158  blin2  24350  met2ndci  24443  zdis  24738  reconnlem2  24749  cnheibor  24887  lebnum  24896  nmoleub2lem  25047  nmoleub2lem3  25048  nmoleub2lem2  25049  nmoleub3  25052  nmhmcn  25053  minveclem4  25365  ovolicc2lem5  25455  ioorcl  25511  ig1peu  26113  taylfvallem1  26297  tayl0  26302  ppisval  27047  ppinprm  27095  chtnprm  27097  chtleppi  27154  pclogsum  27159  chpchtsum  27163  chpub  27164  chebbnd1lem1  27413  chtppilimlem1  27417  rplogsum  27471  perpcom  28693  perpneq  28694  ragperp  28697  tocyc01  33090  cyc3evpm  33122  cycpmgcl  33125  cycpmconjslem2  33127  cyc3conja  33129  idomrcanOLD  33248  unitpidl1  33388  ssdifidlprm  33422  mxidlirredi  33435  mxidlirred  33436  rprmirredb  33496  pidufd  33507  1arithufdlem4  33511  exsslsb  33585  lbsdiflsp0  33615  esum2d  34076  ispisys2  34136  sigapisys  34138  sigapildsyslem  34144  sigapildsys  34145  eulerpartlemgvv  34360  tgoldbachgt  34647  weiunfrlem  36445  weiunfr  36448  fvineqsneq  37393  pibt2  37398  limclner  45642  iinfconstbas  49048  ffthoppf  49147  thincciso  49435  termcterm2  49496  termcciso  49498  termccisoeu  49499  termfucterm  49526  uobeqterm  49528