Theorem elin1d 4128

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  ordtypelem3  9209  ordtypelem4  9210  ordtypelem7  9213  infpwfien  9749  ttukeylem6  10201  fpwwe2lem11  10328  explecnv  15505  smuval2  16117  submrc  17254  coffth  17568  catcbascl  17743  catcoppcclOLD  17749  catcfucclOLD  17751  catcxpcclOLD  17841  acsfiindd  18186  frgpnabllem2  19390  ablfac2  19607  zringlpirlem2  20597  mplind  21188  neiptoptop  22190  restbas  22217  subbascn  22313  cnconn  22481  clsconn  22489  conncompclo  22494  cldllycmp  22554  llycmpkgen2  22609  1stckgenlem  22612  txcls  22663  txcnp  22679  ptcnplem  22680  xkopt  22714  txconn  22748  basqtop  22770  tgqtop  22771  kqnrmlem1  22802  kqnrmlem2  22803  nrmhmph  22853  ptcmplem5  23115  restutop  23297  blin2  23490  met2ndci  23584  zdis  23885  reconnlem2  23896  cnheibor  24024  lebnum  24033  nmoleub2lem  24183  nmoleub2lem3  24184  nmoleub2lem2  24185  nmoleub3  24188  nmhmcn  24189  minveclem4  24501  ovolicc2lem5  24590  ioorcl  24646  ig1peu  25241  taylfvallem1  25421  tayl0  25426  ppisval  26158  ppinprm  26206  chtnprm  26208  chtleppi  26263  pclogsum  26268  chpchtsum  26272  chpub  26273  chebbnd1lem1  26522  chtppilimlem1  26526  rplogsum  26580  perpcom  26978  perpneq  26979  ragperp  26982  tocyc01  31287  cyc3evpm  31319  cycpmgcl  31322  cycpmconjslem2  31324  cyc3conja  31326  lbsdiflsp0  31609  esum2d  31961  ispisys2  32021  sigapisys  32023  sigapildsyslem  32029  sigapildsys  32030  eulerpartlemgvv  32243  tgoldbachgt  32543  fvineqsneq  35510  pibt2  35515  limclner  43082  thincciso  46218