Theorem elin2d 4198

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954

This theorem is referenced by:  f1opwfi  9352  elfiun  9421  ordtypelem3  9511  infpwfien  10053  ttukeylem6  10505  fpwwe2lem11  10632  explecnv  15807  bitsinv1  16379  smuval2  16419  firest  17374  sscres  17766  funcres2c  17848  coffth  17883  rescfth  17884  catcoppccl  18063  catcoppcclOLD  18064  catcfuccl  18065  catcfucclOLD  18066  catcxpccl  18155  catcxpcclOLD  18156  psssdm2  18530  sylow2a  19481  frgpnabllem2  19736  sralmod  20801  2idlridld  20859  zringlpirlem3  21025  mplind  21622  neiptoptop  22626  restbas  22653  ordtrest  22697  subbascn  22749  lmss  22793  cnconn  22917  clsconn  22925  conncompclo  22930  subislly  22976  cldllycmp  22990  1stckgenlem  23048  txcls  23099  txcnp  23115  txtube  23135  txcmplem1  23136  txkgen  23147  xkopt  23150  xkococnlem  23154  txconn  23184  basqtop  23206  tgqtop  23207  kqnrmlem1  23238  kqnrmlem2  23239  nrmhmph  23289  uzrest  23392  alexsubALTlem3  23544  ptcmplem2  23548  tsmslem1  23624  tsmsxplem1  23648  tsmsxplem2  23649  tsmsxp  23650  blin2  23926  met2ndci  24022  zdis  24323  reconnlem2  24334  reconn  24335  xrge0gsumle  24340  cnheibor  24462  lebnum  24471  nmoleub2lem3  24622  nmoleub3  24626  caussi  24805  minveclem4b  24939  minveclem4  24940  ovolfcl  24974  ovolfioo  24975  ovolficc  24976  ovolficcss  24977  ovolfsval  24978  ovoliunlem1  25010  ovolicc2lem4  25028  ovolicc2lem5  25029  uniiccdif  25086  uniioovol  25087  uniiccvol  25088  uniioombllem2a  25090  uniioombllem3a  25092  uniioombllem4  25094  uniioombllem5  25095  uniioombllem6  25096  vitalilem2  25117  vitalilem4  25119  ig1peu  25680  taylfvallem1  25860  tayl0  25865  ppisval  26597  chtf  26601  efchtcl  26604  chtge0  26605  ppinprm  26645  chtprm  26646  chtnprm  26647  chtwordi  26649  chtdif  26651  efchtdvds  26652  chtlepsi  26698  chtleppi  26702  pclogsum  26707  chpval2  26710  chpchtsum  26711  chpub  26712  chebbnd1lem1  26961  chtppilimlem1  26965  rplogsumlem2  26977  perpneq  27954  ragperp  27957  tocyc01  32264  cyc3evpm  32296  cycpmconjslem2  32301  cyc3conja  32303  idomdomd  32361  mxidlirred  32576  ressdeg1  32639  lbsdiflsp0  32699  irngss  32739  esum2d  33079  ispisys2  33139  sigapisys  33141  sigapildsyslem  33147  sigapildsys  33148  sseqf  33379  tgoldbachgt  33663  bnj1172  34000  mhpind  41163  ismnushort  43045  cnrefiisplem  44531  hoiqssbllem3  45326  smflimlem3  45475