Theorem elin1d 4199

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956

This theorem is referenced by:  ordtypelem3  9515  ordtypelem4  9516  ordtypelem7  9519  infpwfien  10057  ttukeylem6  10509  fpwwe2lem11  10636  explecnv  15811  smuval2  16423  submrc  17572  coffth  17887  catcbascl  18062  catcoppcclOLD  18068  catcfucclOLD  18070  catcxpcclOLD  18160  acsfiindd  18506  frgpnabllem2  19742  ablfac2  19959  2idllidld  20866  zringlpirlem2  21033  mplind  21631  neiptoptop  22635  restbas  22662  subbascn  22758  cnconn  22926  clsconn  22934  conncompclo  22939  cldllycmp  22999  llycmpkgen2  23054  1stckgenlem  23057  txcls  23108  txcnp  23124  ptcnplem  23125  xkopt  23159  txconn  23193  basqtop  23215  tgqtop  23216  kqnrmlem1  23247  kqnrmlem2  23248  nrmhmph  23298  ptcmplem5  23560  restutop  23742  blin2  23935  met2ndci  24031  zdis  24332  reconnlem2  24343  cnheibor  24471  lebnum  24480  nmoleub2lem  24630  nmoleub2lem3  24631  nmoleub2lem2  24632  nmoleub3  24635  nmhmcn  24636  minveclem4  24949  ovolicc2lem5  25038  ioorcl  25094  ig1peu  25689  taylfvallem1  25869  tayl0  25874  ppisval  26608  ppinprm  26656  chtnprm  26658  chtleppi  26713  pclogsum  26718  chpchtsum  26722  chpub  26723  chebbnd1lem1  26972  chtppilimlem1  26976  rplogsum  27030  perpcom  27995  perpneq  27996  ragperp  27999  tocyc01  32308  cyc3evpm  32340  cycpmgcl  32343  cycpmconjslem2  32345  cyc3conja  32347  idomringd  32406  idomrcan  32408  unitpidl1  32573  mxidlirredi  32618  mxidlirred  32619  lbsdiflsp0  32742  esum2d  33122  ispisys2  33182  sigapisys  33184  sigapildsyslem  33190  sigapildsys  33191  eulerpartlemgvv  33406  tgoldbachgt  33706  fvineqsneq  36341  pibt2  36346  limclner  44415  thincciso  47717