Theorem elin1d 4197

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

Syntax hints:   → wi 4   ∈ wcel 2104   ∩ cin 3946

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954

This theorem is referenced by:  ordtypelem3  9517  ordtypelem4  9518  ordtypelem7  9521  infpwfien  10059  ttukeylem6  10511  fpwwe2lem11  10638  explecnv  15815  smuval2  16427  submrc  17576  coffth  17891  catcbascl  18066  catcoppcclOLD  18072  catcfucclOLD  18074  catcxpcclOLD  18164  acsfiindd  18510  frgpnabllem2  19783  ablfac2  20000  2idllidld  21015  zringlpirlem2  21234  mplind  21850  neiptoptop  22855  restbas  22882  subbascn  22978  cnconn  23146  clsconn  23154  conncompclo  23159  cldllycmp  23219  llycmpkgen2  23274  1stckgenlem  23277  txcls  23328  txcnp  23344  ptcnplem  23345  xkopt  23379  txconn  23413  basqtop  23435  tgqtop  23436  kqnrmlem1  23467  kqnrmlem2  23468  nrmhmph  23518  ptcmplem5  23780  restutop  23962  blin2  24155  met2ndci  24251  zdis  24552  reconnlem2  24563  cnheibor  24701  lebnum  24710  nmoleub2lem  24861  nmoleub2lem3  24862  nmoleub2lem2  24863  nmoleub3  24866  nmhmcn  24867  minveclem4  25180  ovolicc2lem5  25270  ioorcl  25326  ig1peu  25924  taylfvallem1  26105  tayl0  26110  ppisval  26844  ppinprm  26892  chtnprm  26894  chtleppi  26949  pclogsum  26954  chpchtsum  26958  chpub  26959  chebbnd1lem1  27208  chtppilimlem1  27212  rplogsum  27266  perpcom  28231  perpneq  28232  ragperp  28235  tocyc01  32547  cyc3evpm  32579  cycpmgcl  32582  cycpmconjslem2  32584  cyc3conja  32586  idomringd  32645  idomrcan  32647  unitpidl1  32816  mxidlirredi  32861  mxidlirred  32862  lbsdiflsp0  32999  esum2d  33389  ispisys2  33449  sigapisys  33451  sigapildsyslem  33457  sigapildsys  33458  eulerpartlemgvv  33673  tgoldbachgt  33973  fvineqsneq  36596  pibt2  36601  limclner  44665  thincciso  47756