Theorem elin1d 4227

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  ordtypelem3  9589  ordtypelem4  9590  ordtypelem7  9593  infpwfien  10131  ttukeylem6  10583  fpwwe2lem11  10710  explecnv  15913  smuval2  16528  submrc  17686  coffth  18003  catcbascl  18179  catcoppcclOLD  18185  catcfucclOLD  18187  catcxpcclOLD  18277  acsfiindd  18623  frgpnabllem2  19916  ablfac2  20133  idomcringd  20749  2idllidld  21287  zringlpirlem2  21497  mplind  22117  neiptoptop  23160  restbas  23187  subbascn  23283  cnconn  23451  clsconn  23459  conncompclo  23464  cldllycmp  23524  llycmpkgen2  23579  1stckgenlem  23582  txcls  23633  txcnp  23649  ptcnplem  23650  xkopt  23684  txconn  23718  basqtop  23740  tgqtop  23741  kqnrmlem1  23772  kqnrmlem2  23773  nrmhmph  23823  ptcmplem5  24085  restutop  24267  blin2  24460  met2ndci  24556  zdis  24857  reconnlem2  24868  cnheibor  25006  lebnum  25015  nmoleub2lem  25166  nmoleub2lem3  25167  nmoleub2lem2  25168  nmoleub3  25171  nmhmcn  25172  minveclem4  25485  ovolicc2lem5  25575  ioorcl  25631  ig1peu  26234  taylfvallem1  26416  tayl0  26421  ppisval  27165  ppinprm  27213  chtnprm  27215  chtleppi  27272  pclogsum  27277  chpchtsum  27281  chpub  27282  chebbnd1lem1  27531  chtppilimlem1  27535  rplogsum  27589  perpcom  28739  perpneq  28740  ragperp  28743  tocyc01  33111  cyc3evpm  33143  cycpmgcl  33146  cycpmconjslem2  33148  cyc3conja  33150  idomrcanOLD  33251  unitpidl1  33417  ssdifidlprm  33451  mxidlirredi  33464  mxidlirred  33465  rprmirredb  33525  pidufd  33536  1arithufdlem4  33540  lbsdiflsp0  33639  esum2d  34057  ispisys2  34117  sigapisys  34119  sigapildsyslem  34125  sigapildsys  34126  eulerpartlemgvv  34341  tgoldbachgt  34640  weiunfrlem  36430  weiunfr  36433  fvineqsneq  37378  pibt2  37383  limclner  45572  thincciso  48716