Theorem elin2d 4168

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  f1opwfi  9307  elfiun  9381  ordtypelem3  9473  infpwfien  10015  ttukeylem6  10467  fpwwe2lem11  10594  explecnv  15831  bitsinv1  16412  smuval2  16452  firest  17395  sscres  17785  funcres2c  17865  coffth  17900  rescfth  17901  catcoppccl  18079  catcfuccl  18080  catcxpccl  18168  psssdm2  18540  sylow2a  19549  frgpnabllem2  19804  idomdomd  20635  sralmod  21094  2idlridld  21165  zringlpirlem3  21374  mplind  21977  neiptoptop  23018  restbas  23045  ordtrest  23089  subbascn  23141  lmss  23185  cnconn  23309  clsconn  23317  conncompclo  23322  subislly  23368  cldllycmp  23382  1stckgenlem  23440  txcls  23491  txcnp  23507  txtube  23527  txcmplem1  23528  txkgen  23539  xkopt  23542  xkococnlem  23546  txconn  23576  basqtop  23598  tgqtop  23599  kqnrmlem1  23630  kqnrmlem2  23631  nrmhmph  23681  uzrest  23784  alexsubALTlem3  23936  ptcmplem2  23940  tsmslem1  24016  tsmsxplem1  24040  tsmsxplem2  24041  tsmsxp  24042  blin2  24317  met2ndci  24410  zdis  24705  reconnlem2  24716  reconn  24717  xrge0gsumle  24722  cnheibor  24854  lebnum  24863  nmoleub2lem3  25015  nmoleub3  25019  caussi  25197  minveclem4b  25331  minveclem4  25332  ovolfcl  25367  ovolfioo  25368  ovolficc  25369  ovolficcss  25370  ovolfsval  25371  ovoliunlem1  25403  ovolicc2lem4  25421  ovolicc2lem5  25422  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2a  25483  uniioombllem3a  25485  uniioombllem4  25487  uniioombllem5  25488  uniioombllem6  25489  vitalilem2  25510  vitalilem4  25512  ig1peu  26080  taylfvallem1  26264  tayl0  26269  ppisval  27014  chtf  27018  efchtcl  27021  chtge0  27022  ppinprm  27062  chtprm  27063  chtnprm  27064  chtwordi  27066  chtdif  27068  efchtdvds  27069  chtlepsi  27117  chtleppi  27121  pclogsum  27126  chpval2  27129  chpchtsum  27130  chpub  27131  chebbnd1lem1  27380  chtppilimlem1  27384  rplogsumlem2  27396  perpneq  28641  ragperp  28644  tocyc01  33075  cyc3evpm  33107  cycpmconjslem2  33112  cyc3conja  33114  ssdifidlprm  33429  mxidlirred  33443  pidufd  33514  1arithufdlem4  33518  ressdeg1  33535  exsslsb  33592  lbsdiflsp0  33622  irngss  33682  rtelextdg2lem  33716  esum2d  34083  ispisys2  34143  sigapisys  34145  sigapildsyslem  34151  sigapildsys  34152  sseqf  34383  tgoldbachgt  34654  bnj1172  34991  weiunfrlem  36452  mhpind  42582  ismnushort  44290  cnrefiisplem  45827  hoiqssbllem3  46622  smflimlem3  46771  iinfconstbas  49055  ffthoppf  49154  fucoppc  49399  termcterm  49502  termcterm2  49503