Theorem elin1d 4104

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  ordtypelem3  9551  ordtypelem4  9552  ordtypelem7  9555  infpwfien  10180  ttukeylem6  10631  fpwwe2lem11  10765  explecnv  16078  smuval2  16696  submrc  17852  coffth  18163  catcbascl  18337  acsfiindd  18777  frgpnabllem2  20139  ablfac2  20356  idomcringd  21029  2idllidld  21598  ssdifidlprm  21693  zringlpirlem2  21824  mplind  22434  neiptoptop  23504  restbas  23531  subbascn  23627  cnconn  23795  clsconn  23803  conncompclo  23808  cldllycmp  23869  llycmpkgen2  23924  1stckgenlem  23927  txcls  23978  txcnp  23994  ptcnplem  23995  xkopt  24029  txconn  24063  basqtop  24085  tgqtop  24086  kqnrmlem1  24117  kqnrmlem2  24118  nrmhmph  24168  ptcmplem5  24430  restutop  24611  blin2  24803  met2ndci  24896  zdis  25191  reconnlem2  25202  cnheibor  25331  lebnum  25340  nmoleub2lem  25490  nmoleub2lem3  25491  nmoleub2lem2  25492  nmoleub3  25495  nmhmcn  25496  minveclem4  25808  ovolicc2lem5  25897  ioorcl  25953  ig1peu  26548  taylfvallem1  26741  tayl0  26746  ppisval  27488  ppinprm  27536  chtnprm  27538  chtleppi  27594  pclogsum  27599  chpchtsum  27603  chpub  27604  chebbnd1lem1  27853  chtppilimlem1  27857  rplogsum  27911  tglnpt4  29180  perpcom  29245  perpneq  29246  ragperp  29249  lnincplng  29319  angmgmaddeu1  29436  perpprlng  29485  prlngplngtr  29494  quadcgrprlng  29501  tocyc01  33778  cyc3evpm  33810  cycpmgcl  33813  cycpmconjslem2  33815  cyc3conja  33817  mxidlirred  34101  dflringlem3  34132  dflring4  34134  rprmirredb  34168  pidufd  34179  1arithufdlem4  34183  exsslsb  34340  lbsdiflsp0  34369  cmpcref  34593  esum2d  34836  ispisys2  34897  sigapisys  34899  sigapildsyslem  34905  sigapildsys  34906  eulerpartlemgvv  35119  tgoldbachgt  35403  weiunfrlem  37467  weiunfr  37470  dfttc4  37533  fvineqsneq  38603  pibt2  38608  limclner  46934  fourierdlem49  47438  tmachlem-agreeprod  48220  tmachlem-exagreecover  48229  iinfconstbas  50511  ffthoppf  50612  thincciso  50919  termcterm2  50980  termcciso  50982  termccisoeu  50983  termfucterm  51013  uobeqterm  51015