Theorem elin1d 4125

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888

This theorem is referenced by:  ordtypelem3  8968  ordtypelem4  8969  ordtypelem7  8972  infpwfien  9473  ttukeylem6  9925  fpwwe2lem12  10052  explecnv  15212  smuval2  15821  submrc  16891  coffth  17198  catcoppccl  17360  catcfuccl  17361  catcxpccl  17449  acsfiindd  17779  frgpnabllem2  18987  ablfac2  19204  zringlpirlem2  20178  mplind  20741  neiptoptop  21736  restbas  21763  subbascn  21859  cnconn  22027  clsconn  22035  conncompclo  22040  cldllycmp  22100  llycmpkgen2  22155  1stckgenlem  22158  txcls  22209  txcnp  22225  ptcnplem  22226  xkopt  22260  txconn  22294  basqtop  22316  tgqtop  22317  kqnrmlem1  22348  kqnrmlem2  22349  nrmhmph  22399  ptcmplem5  22661  restutop  22843  blin2  23036  met2ndci  23129  zdis  23421  reconnlem2  23432  cnheibor  23560  lebnum  23569  nmoleub2lem  23719  nmoleub2lem3  23720  nmoleub2lem2  23721  nmoleub3  23724  nmhmcn  23725  minveclem4  24036  ovolicc2lem5  24125  ioorcl  24181  ig1peu  24772  taylfvallem1  24952  tayl0  24957  ppisval  25689  ppinprm  25737  chtnprm  25739  chtleppi  25794  pclogsum  25799  chpchtsum  25803  chpub  25804  chebbnd1lem1  26053  chtppilimlem1  26057  rplogsum  26111  perpcom  26507  perpneq  26508  ragperp  26511  tocyc01  30810  cyc3evpm  30842  cycpmgcl  30845  cycpmconjslem2  30847  cyc3conja  30849  lbsdiflsp0  31110  esum2d  31462  ispisys2  31522  sigapisys  31524  sigapildsyslem  31530  sigapildsys  31531  eulerpartlemgvv  31744  tgoldbachgt  32044  fvineqsneq  34829  pibt2  34834  limclner  42293