Theorem elin1d 4163

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3910

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918

This theorem is referenced by:  ordtypelem3  9449  ordtypelem4  9450  ordtypelem7  9453  infpwfien  9991  ttukeylem6  10443  fpwwe2lem11  10570  explecnv  15807  smuval2  16428  submrc  17565  coffth  17876  catcbascl  18050  acsfiindd  18488  frgpnabllem2  19780  ablfac2  19997  idomcringd  20612  2idllidld  21140  zringlpirlem2  21349  mplind  21953  neiptoptop  22994  restbas  23021  subbascn  23117  cnconn  23285  clsconn  23293  conncompclo  23298  cldllycmp  23358  llycmpkgen2  23413  1stckgenlem  23416  txcls  23467  txcnp  23483  ptcnplem  23484  xkopt  23518  txconn  23552  basqtop  23574  tgqtop  23575  kqnrmlem1  23606  kqnrmlem2  23607  nrmhmph  23657  ptcmplem5  23919  restutop  24101  blin2  24293  met2ndci  24386  zdis  24681  reconnlem2  24692  cnheibor  24830  lebnum  24839  nmoleub2lem  24990  nmoleub2lem3  24991  nmoleub2lem2  24992  nmoleub3  24995  nmhmcn  24996  minveclem4  25308  ovolicc2lem5  25398  ioorcl  25454  ig1peu  26056  taylfvallem1  26240  tayl0  26245  ppisval  26990  ppinprm  27038  chtnprm  27040  chtleppi  27097  pclogsum  27102  chpchtsum  27106  chpub  27107  chebbnd1lem1  27356  chtppilimlem1  27360  rplogsum  27414  perpcom  28616  perpneq  28617  ragperp  28620  tocyc01  33048  cyc3evpm  33080  cycpmgcl  33083  cycpmconjslem2  33085  cyc3conja  33087  idomrcanOLD  33205  unitpidl1  33368  ssdifidlprm  33402  mxidlirredi  33415  mxidlirred  33416  rprmirredb  33476  pidufd  33487  1arithufdlem4  33491  exsslsb  33565  lbsdiflsp0  33595  esum2d  34056  ispisys2  34116  sigapisys  34118  sigapildsyslem  34124  sigapildsys  34125  eulerpartlemgvv  34340  tgoldbachgt  34627  weiunfrlem  36425  weiunfr  36428  fvineqsneq  37373  pibt2  37378  limclner  45622  iinfconstbas  49028  ffthoppf  49127  thincciso  49415  termcterm2  49476  termcciso  49478  termccisoeu  49479  termfucterm  49506  uobeqterm  49508