Theorem elin1d 4100

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090

This theorem is used by:  ordtypelem3  9521  ordtypelem4  9522  ordtypelem7  9525  infpwfien  10148  ttukeylem6  10599  fpwwe2lem11  10733  explecnv  16043  smuval2  16661  submrc  17811  coffth  18122  catcbascl  18296  acsfiindd  18736  frgpnabllem2  20097  ablfac2  20314  idomcringd  20987  2idllidld  21556  ssdifidlprm  21651  zringlpirlem2  21778  mplind  22388  neiptoptop  23458  restbas  23485  subbascn  23581  cnconn  23749  clsconn  23757  conncompclo  23762  cldllycmp  23823  llycmpkgen2  23878  1stckgenlem  23881  txcls  23932  txcnp  23948  ptcnplem  23949  xkopt  23983  txconn  24017  basqtop  24039  tgqtop  24040  kqnrmlem1  24071  kqnrmlem2  24072  nrmhmph  24122  ptcmplem5  24384  restutop  24565  blin2  24757  met2ndci  24850  zdis  25145  reconnlem2  25156  cnheibor  25285  lebnum  25294  nmoleub2lem  25444  nmoleub2lem3  25445  nmoleub2lem2  25446  nmoleub3  25449  nmhmcn  25450  minveclem4  25762  ovolicc2lem5  25851  ioorcl  25907  ig1peu  26502  taylfvallem1  26693  tayl0  26698  ppisval  27440  ppinprm  27488  chtnprm  27490  chtleppi  27546  pclogsum  27551  chpchtsum  27555  chpub  27556  chebbnd1lem1  27805  chtppilimlem1  27809  rplogsum  27863  tglnpt4  29132  perpcom  29197  perpneq  29198  ragperp  29201  lnincplng  29271  angmgmaddeu1  29388  perpprlng  29437  prlngplngtr  29446  quadcgrprlng  29453  tocyc01  33729  cyc3evpm  33761  cycpmgcl  33764  cycpmconjslem2  33766  cyc3conja  33768  mxidlirred  34047  dflringlem3  34078  dflring4  34080  rprmirredb  34114  pidufd  34125  1arithufdlem4  34129  exsslsb  34279  lbsdiflsp0  34308  cmpcref  34532  esum2d  34775  ispisys2  34836  sigapisys  34838  sigapildsyslem  34844  sigapildsys  34845  eulerpartlemgvv  35058  tgoldbachgt  35342  weiunfrlem  37376  weiunfr  37379  dfttc4  37442  fvineqsneq  38472  pibt2  38477  limclner  46797  fourierdlem49  47301  tmachlem-agreeprod  48083  tmachlem-exagreecover  48092  iinfconstbas  50316  ffthoppf  50417  thincciso  50724  termcterm2  50785  termcciso  50787  termccisoeu  50788  termfucterm  50818  uobeqterm  50820