Theorem elin1d 4179

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

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

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933

This theorem is referenced by:  ordtypelem3  9532  ordtypelem4  9533  ordtypelem7  9536  infpwfien  10074  ttukeylem6  10526  fpwwe2lem11  10653  explecnv  15879  smuval2  16499  submrc  17638  coffth  17949  catcbascl  18123  acsfiindd  18561  frgpnabllem2  19853  ablfac2  20070  idomcringd  20685  2idllidld  21213  zringlpirlem2  21422  mplind  22026  neiptoptop  23067  restbas  23094  subbascn  23190  cnconn  23358  clsconn  23366  conncompclo  23371  cldllycmp  23431  llycmpkgen2  23486  1stckgenlem  23489  txcls  23540  txcnp  23556  ptcnplem  23557  xkopt  23591  txconn  23625  basqtop  23647  tgqtop  23648  kqnrmlem1  23679  kqnrmlem2  23680  nrmhmph  23730  ptcmplem5  23992  restutop  24174  blin2  24366  met2ndci  24459  zdis  24754  reconnlem2  24765  cnheibor  24903  lebnum  24912  nmoleub2lem  25063  nmoleub2lem3  25064  nmoleub2lem2  25065  nmoleub3  25068  nmhmcn  25069  minveclem4  25382  ovolicc2lem5  25472  ioorcl  25528  ig1peu  26130  taylfvallem1  26314  tayl0  26319  ppisval  27064  ppinprm  27112  chtnprm  27114  chtleppi  27171  pclogsum  27176  chpchtsum  27180  chpub  27181  chebbnd1lem1  27430  chtppilimlem1  27434  rplogsum  27488  perpcom  28638  perpneq  28639  ragperp  28642  tocyc01  33075  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  idomrcanOLD  33222  unitpidl1  33385  ssdifidlprm  33419  mxidlirredi  33432  mxidlirred  33433  rprmirredb  33493  pidufd  33504  1arithufdlem4  33508  exsslsb  33582  lbsdiflsp0  33612  esum2d  34070  ispisys2  34130  sigapisys  34132  sigapildsyslem  34138  sigapildsys  34139  eulerpartlemgvv  34354  tgoldbachgt  34641  weiunfrlem  36428  weiunfr  36431  fvineqsneq  37376  pibt2  37381  limclner  45628  iinfconstbas  48981  thincciso  49287  termcterm2  49347  termcciso  49349  termccisoeu  49350