Theorem elin2d 4157

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  f1opwfi  9256  elfiun  9333  ordtypelem3  9425  infpwfien  9972  ttukeylem6  10424  fpwwe2lem11  10552  explecnv  15788  bitsinv1  16369  smuval2  16409  firest  17352  sscres  17747  funcres2c  17827  coffth  17862  rescfth  17863  catcoppccl  18041  catcfuccl  18042  catcxpccl  18130  psssdm2  18504  sylow2a  19548  frgpnabllem2  19803  idomdomd  20659  sralmod  21139  2idlridld  21210  zringlpirlem3  21419  mplind  22025  neiptoptop  23075  restbas  23102  ordtrest  23146  subbascn  23198  lmss  23242  cnconn  23366  clsconn  23374  conncompclo  23379  subislly  23425  cldllycmp  23439  1stckgenlem  23497  txcls  23548  txcnp  23564  txtube  23584  txcmplem1  23585  txkgen  23596  xkopt  23599  xkococnlem  23603  txconn  23633  basqtop  23655  tgqtop  23656  kqnrmlem1  23687  kqnrmlem2  23688  nrmhmph  23738  uzrest  23841  alexsubALTlem3  23993  ptcmplem2  23997  tsmslem1  24073  tsmsxplem1  24097  tsmsxplem2  24098  tsmsxp  24099  blin2  24373  met2ndci  24466  zdis  24761  reconnlem2  24772  reconn  24773  xrge0gsumle  24778  cnheibor  24910  lebnum  24919  nmoleub2lem3  25071  nmoleub3  25075  caussi  25253  minveclem4b  25387  minveclem4  25388  ovolfcl  25423  ovolfioo  25424  ovolficc  25425  ovolficcss  25426  ovolfsval  25427  ovoliunlem1  25459  ovolicc2lem4  25477  ovolicc2lem5  25478  uniiccdif  25535  uniioovol  25536  uniiccvol  25537  uniioombllem2a  25539  uniioombllem3a  25541  uniioombllem4  25543  uniioombllem5  25544  uniioombllem6  25545  vitalilem2  25566  vitalilem4  25568  ig1peu  26136  taylfvallem1  26320  tayl0  26325  ppisval  27070  chtf  27074  efchtcl  27077  chtge0  27078  ppinprm  27118  chtprm  27119  chtnprm  27120  chtwordi  27122  chtdif  27124  efchtdvds  27125  chtlepsi  27173  chtleppi  27177  pclogsum  27182  chpval2  27185  chpchtsum  27186  chpub  27187  chebbnd1lem1  27436  chtppilimlem1  27440  rplogsumlem2  27452  perpneq  28786  ragperp  28789  tocyc01  33200  cyc3evpm  33232  cycpmconjslem2  33237  cyc3conja  33239  ssdifidlprm  33539  mxidlirred  33553  pidufd  33624  1arithufdlem4  33628  ressdeg1  33647  exsslsb  33753  lbsdiflsp0  33783  irngss  33844  rtelextdg2lem  33883  esum2d  34250  ispisys2  34310  sigapisys  34312  sigapildsyslem  34318  sigapildsys  34319  sseqf  34549  tgoldbachgt  34820  bnj1172  35157  weiunfrlem  36658  mhpind  42837  ismnushort  44542  cnrefiisplem  46073  hoiqssbllem3  46868  smflimlem3  47017  iinfconstbas  49311  ffthoppf  49410  fucoppc  49655  termcterm  49758  termcterm2  49759