Theorem elin1d 4145

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  ordtypelem3  9429  ordtypelem4  9430  ordtypelem7  9433  infpwfien  9978  ttukeylem6  10430  fpwwe2lem11  10558  explecnv  15824  smuval2  16445  submrc  17588  coffth  17899  catcbascl  18073  acsfiindd  18513  frgpnabllem2  19843  ablfac2  20060  idomcringd  20698  2idllidld  21247  zringlpirlem2  21456  mplind  22061  neiptoptop  23109  restbas  23136  subbascn  23232  cnconn  23400  clsconn  23408  conncompclo  23413  cldllycmp  23473  llycmpkgen2  23528  1stckgenlem  23531  txcls  23582  txcnp  23598  ptcnplem  23599  xkopt  23633  txconn  23667  basqtop  23689  tgqtop  23690  kqnrmlem1  23721  kqnrmlem2  23722  nrmhmph  23772  ptcmplem5  24034  restutop  24215  blin2  24407  met2ndci  24500  zdis  24795  reconnlem2  24806  cnheibor  24935  lebnum  24944  nmoleub2lem  25094  nmoleub2lem3  25095  nmoleub2lem2  25096  nmoleub3  25099  nmhmcn  25100  minveclem4  25412  ovolicc2lem5  25501  ioorcl  25557  ig1peu  26153  taylfvallem1  26336  tayl0  26341  ppisval  27084  ppinprm  27132  chtnprm  27134  chtleppi  27190  pclogsum  27195  chpchtsum  27199  chpub  27200  chebbnd1lem1  27449  chtppilimlem1  27453  rplogsum  27507  perpcom  28798  perpneq  28799  ragperp  28802  tocyc01  33197  cyc3evpm  33229  cycpmgcl  33232  cycpmconjslem2  33234  cyc3conja  33236  idomrcanOLD  33361  unitpidl1  33502  ssdifidlprm  33536  mxidlirredi  33549  mxidlirred  33550  rprmirredb  33610  pidufd  33621  1arithufdlem4  33625  exsslsb  33759  lbsdiflsp0  33789  esum2d  34256  ispisys2  34316  sigapisys  34318  sigapildsyslem  34324  sigapildsys  34325  eulerpartlemgvv  34539  tgoldbachgt  34826  weiunfrlem  36665  weiunfr  36668  dfttc4  36731  fvineqsneq  37745  pibt2  37750  limclner  46100  iinfconstbas  49556  ffthoppf  49655  thincciso  49943  termcterm2  50004  termcciso  50006  termccisoeu  50007  termfucterm  50034  uobeqterm  50036