Theorem elin1d 4088

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-in 3850

This theorem is referenced by:  ordtypelem3  9059  ordtypelem4  9060  ordtypelem7  9063  infpwfien  9564  ttukeylem6  10016  fpwwe2lem11  10143  explecnv  15315  smuval2  15927  submrc  17004  coffth  17313  catcoppccl  17486  catcfuccl  17487  catcxpccl  17575  acsfiindd  17905  frgpnabllem2  19115  ablfac2  19332  zringlpirlem2  20306  mplind  20884  neiptoptop  21884  restbas  21911  subbascn  22007  cnconn  22175  clsconn  22183  conncompclo  22188  cldllycmp  22248  llycmpkgen2  22303  1stckgenlem  22306  txcls  22357  txcnp  22373  ptcnplem  22374  xkopt  22408  txconn  22442  basqtop  22464  tgqtop  22465  kqnrmlem1  22496  kqnrmlem2  22497  nrmhmph  22547  ptcmplem5  22809  restutop  22991  blin2  23184  met2ndci  23277  zdis  23570  reconnlem2  23581  cnheibor  23709  lebnum  23718  nmoleub2lem  23868  nmoleub2lem3  23869  nmoleub2lem2  23870  nmoleub3  23873  nmhmcn  23874  minveclem4  24186  ovolicc2lem5  24275  ioorcl  24331  ig1peu  24926  taylfvallem1  25106  tayl0  25111  ppisval  25843  ppinprm  25891  chtnprm  25893  chtleppi  25948  pclogsum  25953  chpchtsum  25957  chpub  25958  chebbnd1lem1  26207  chtppilimlem1  26211  rplogsum  26265  perpcom  26661  perpneq  26662  ragperp  26665  tocyc01  30964  cyc3evpm  30996  cycpmgcl  30999  cycpmconjslem2  31001  cyc3conja  31003  lbsdiflsp0  31281  esum2d  31633  ispisys2  31693  sigapisys  31695  sigapildsyslem  31701  sigapildsys  31702  eulerpartlemgvv  31915  tgoldbachgt  32215  fvineqsneq  35228  pibt2  35233  limclner  42756