Theorem elin1d 4194

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

Syntax hints:   → wi 4   ∈ wcel 2099   ∩ cin 3943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951

This theorem is referenced by:  ordtypelem3  9535  ordtypelem4  9536  ordtypelem7  9539  infpwfien  10077  ttukeylem6  10529  fpwwe2lem11  10656  explecnv  15835  smuval2  16448  submrc  17599  coffth  17916  catcbascl  18092  catcoppcclOLD  18098  catcfucclOLD  18100  catcxpcclOLD  18190  acsfiindd  18536  frgpnabllem2  19820  ablfac2  20037  2idllidld  21137  idomringd  21244  zringlpirlem2  21376  mplind  22001  neiptoptop  23022  restbas  23049  subbascn  23145  cnconn  23313  clsconn  23321  conncompclo  23326  cldllycmp  23386  llycmpkgen2  23441  1stckgenlem  23444  txcls  23495  txcnp  23511  ptcnplem  23512  xkopt  23546  txconn  23580  basqtop  23602  tgqtop  23603  kqnrmlem1  23634  kqnrmlem2  23635  nrmhmph  23685  ptcmplem5  23947  restutop  24129  blin2  24322  met2ndci  24418  zdis  24719  reconnlem2  24730  cnheibor  24868  lebnum  24877  nmoleub2lem  25028  nmoleub2lem3  25029  nmoleub2lem2  25030  nmoleub3  25033  nmhmcn  25034  minveclem4  25347  ovolicc2lem5  25437  ioorcl  25493  ig1peu  26096  taylfvallem1  26278  tayl0  26283  ppisval  27023  ppinprm  27071  chtnprm  27073  chtleppi  27130  pclogsum  27135  chpchtsum  27139  chpub  27140  chebbnd1lem1  27389  chtppilimlem1  27393  rplogsum  27447  perpcom  28504  perpneq  28505  ragperp  28508  tocyc01  32817  cyc3evpm  32849  cycpmgcl  32852  cycpmconjslem2  32854  cyc3conja  32856  idomrcan  32915  unitpidl1  33075  mxidlirredi  33120  mxidlirred  33121  lbsdiflsp0  33256  esum2d  33648  ispisys2  33708  sigapisys  33710  sigapildsyslem  33716  sigapildsys  33717  eulerpartlemgvv  33932  tgoldbachgt  34231  fvineqsneq  36827  pibt2  36832  limclner  44962  thincciso  47978