Theorem elin1d 4199

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956

This theorem is referenced by:  ordtypelem3  9515  ordtypelem4  9516  ordtypelem7  9519  infpwfien  10057  ttukeylem6  10509  fpwwe2lem11  10636  explecnv  15811  smuval2  16423  submrc  17572  coffth  17887  catcbascl  18062  catcoppcclOLD  18068  catcfucclOLD  18070  catcxpcclOLD  18160  acsfiindd  18506  frgpnabllem2  19742  ablfac2  19959  2idllidld  20866  zringlpirlem2  21033  mplind  21631  neiptoptop  22635  restbas  22662  subbascn  22758  cnconn  22926  clsconn  22934  conncompclo  22939  cldllycmp  22999  llycmpkgen2  23054  1stckgenlem  23057  txcls  23108  txcnp  23124  ptcnplem  23125  xkopt  23159  txconn  23193  basqtop  23215  tgqtop  23216  kqnrmlem1  23247  kqnrmlem2  23248  nrmhmph  23298  ptcmplem5  23560  restutop  23742  blin2  23935  met2ndci  24031  zdis  24332  reconnlem2  24343  cnheibor  24471  lebnum  24480  nmoleub2lem  24630  nmoleub2lem3  24631  nmoleub2lem2  24632  nmoleub3  24635  nmhmcn  24636  minveclem4  24949  ovolicc2lem5  25038  ioorcl  25094  ig1peu  25689  taylfvallem1  25869  tayl0  25874  ppisval  26608  ppinprm  26656  chtnprm  26658  chtleppi  26713  pclogsum  26718  chpchtsum  26722  chpub  26723  chebbnd1lem1  26972  chtppilimlem1  26976  rplogsum  27030  perpcom  27964  perpneq  27965  ragperp  27968  tocyc01  32277  cyc3evpm  32309  cycpmgcl  32312  cycpmconjslem2  32314  cyc3conja  32316  idomringd  32375  idomrcan  32377  unitpidl1  32542  mxidlirredi  32587  mxidlirred  32588  lbsdiflsp0  32711  esum2d  33091  ispisys2  33151  sigapisys  33153  sigapildsyslem  33159  sigapildsys  33160  eulerpartlemgvv  33375  tgoldbachgt  33675  fvineqsneq  36293  pibt2  36298  limclner  44367  thincciso  47669