Theorem elin2d 4102

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
elin2d	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Proof of Theorem elin2d

Step	Hyp	Ref	Expression
1		elin1d.1	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))
2		elinel2 4099	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) → 𝑋 ∈ 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝑋 ∈ 𝐵)

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

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 4091

This theorem is used by:  f1opwfi  9349  elfiun  9426  ordtypelem3  9518  infpwfien  10145  ttukeylem6  10596  fpwwe2lem11  10730  explecnv  16040  bitsinv1  16618  smuval2  16658  firest  17609  sscres  18004  funcres2c  18084  coffth  18119  rescfth  18120  catcoppccl  18298  catcfuccl  18299  catcxpccl  18387  psssdm2  18761  sylow2a  19839  frgpnabllem2  20094  idomdomd  20983  sralmod  21468  2idlridld  21554  ssdifidlprm  21648  zringlpirlem3  21776  mplind  22385  neiptoptop  23455  restbas  23482  ordtrest  23526  subbascn  23578  lmss  23622  cnconn  23746  clsconn  23754  conncompclo  23759  subislly  23806  cldllycmp  23820  1stckgenlem  23878  txcls  23929  txcnp  23945  txtube  23965  txcmplem1  23966  txkgen  23977  xkopt  23980  xkococnlem  23984  txconn  24014  basqtop  24036  tgqtop  24037  kqnrmlem1  24068  kqnrmlem2  24069  nrmhmph  24119  uzrest  24222  alexsubALTlem3  24374  ptcmplem2  24378  tsmslem1  24454  tsmsxplem1  24478  tsmsxplem2  24479  tsmsxp  24480  blin2  24754  met2ndci  24847  zdis  25142  reconnlem2  25153  reconn  25154  xrge0gsumle  25159  cnheibor  25282  lebnum  25291  nmoleub2lem3  25442  nmoleub3  25446  caussi  25624  minveclem4b  25758  minveclem4  25759  ovolfcl  25793  ovolfioo  25794  ovolficc  25795  ovolficcss  25796  ovolfsval  25797  ovoliunlem1  25829  ovolicc2lem4  25847  ovolicc2lem5  25848  uniiccdif  25905  uniioovol  25906  uniiccvol  25907  uniioombllem2a  25909  uniioombllem3a  25911  uniioombllem4  25913  uniioombllem5  25914  uniioombllem6  25915  vitalilem2  25936  vitalilem4  25938  ig1peu  26499  taylfvallem1  26690  tayl0  26695  ppisval  27437  chtf  27441  efchtcl  27444  chtge0  27445  ppinprm  27485  chtprm  27486  chtnprm  27487  chtwordi  27489  chtdif  27491  efchtdvds  27492  chtlepsi  27539  chtleppi  27543  pclogsum  27548  chpval2  27551  chpchtsum  27552  chpub  27553  chebbnd1lem1  27802  chtppilimlem1  27806  rplogsumlem2  27818  tglnpt4  29129  perpneq  29195  ragperp  29198  lnincplng  29268  angmgmaddeu1  29385  perpprlng  29434  prlngplngtr  29443  quadcgrprlng  29450  tocyc01  33726  cyc3evpm  33758  cycpmconjslem2  33763  cyc3conja  33765  mxidlirred  34044  dflringlem3  34075  dflring4  34077  pidufd  34122  1arithufdlem4  34126  ressdeg1  34145  exsslsb  34276  lbsdiflsp0  34305  irngss  34366  rtelextdg2lem  34405  cmpcref  34529  esum2d  34772  ispisys2  34833  sigapisys  34835  sigapildsyslem  34841  sigapildsys  34842  sseqf  35071  tgoldbachgt  35339  bnj1172  35678  weiunfrlem  37345  dfttc4  37411  mhpind  43716  ismnushort  45379  cnrefiisplem  46933  hoiqssbllem3  47728  sssmf  47842  smflimlem3  47877  tmachlem-finscan  48039  tmachlem-exagreecover  48050  iinfconstbas  50274  ffthoppf  50375  fucoppc  50639  termcterm  50742  termcterm2  50743