Theorem elin1d 4157

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  ordtypelem3  9489  ordtypelem4  9490  ordtypelem7  9493  infpwfien  10062  ttukeylem6  10513  fpwwe2lem11  10641  explecnv  15942  smuval2  16562  submrc  17706  coffth  18017  catcbascl  18191  acsfiindd  18631  frgpnabllem2  19988  ablfac2  20205  idomcringd  20875  2idllidld  21443  ssdifidlprm  21536  zringlpirlem2  21663  mplind  22271  neiptoptop  23338  restbas  23365  subbascn  23461  cnconn  23629  clsconn  23637  conncompclo  23642  cldllycmp  23703  llycmpkgen2  23758  1stckgenlem  23761  txcls  23812  txcnp  23828  ptcnplem  23829  xkopt  23863  txconn  23897  basqtop  23919  tgqtop  23920  kqnrmlem1  23951  kqnrmlem2  23952  nrmhmph  24002  ptcmplem5  24264  restutop  24445  blin2  24637  met2ndci  24730  zdis  25025  reconnlem2  25036  cnheibor  25165  lebnum  25174  nmoleub2lem  25324  nmoleub2lem3  25325  nmoleub2lem2  25326  nmoleub3  25329  nmhmcn  25330  minveclem4  25642  ovolicc2lem5  25731  ioorcl  25787  ig1peu  26383  taylfvallem1  26571  tayl0  26576  ppisval  27319  ppinprm  27367  chtnprm  27369  chtleppi  27425  pclogsum  27430  chpchtsum  27434  chpub  27435  chebbnd1lem1  27684  chtppilimlem1  27688  rplogsum  27742  tglnpt4  28979  perpcom  29044  perpneq  29045  ragperp  29048  lnincplng  29117  perpprlng  29255  prlngplngtr  29264  quadcgrprlng  29271  tocyc01  33502  cyc3evpm  33534  cycpmgcl  33537  cycpmconjslem2  33539  cyc3conja  33541  mxidlirred  33819  dflringlem3  33850  dflring4  33852  rprmirredb  33886  pidufd  33897  1arithufdlem4  33901  exsslsb  34051  lbsdiflsp0  34080  esum2d  34547  ispisys2  34608  sigapisys  34610  sigapildsyslem  34616  sigapildsys  34617  eulerpartlemgvv  34831  tgoldbachgt  35115  weiunfrlem  37032  weiunfr  37035  dfttc4  37098  fvineqsneq  38115  pibt2  38120  limclner  46423  fourierdlem49  46927  iinfconstbas  49901  ffthoppf  50000  thincciso  50288  termcterm2  50349  termcciso  50351  termccisoeu  50352  termfucterm  50379  uobeqterm  50381