Theorem elin2d 4164

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

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

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 3446  df-in 3918

This theorem is referenced by:  f1opwfi  9283  elfiun  9357  ordtypelem3  9449  infpwfien  9991  ttukeylem6  10443  fpwwe2lem11  10570  explecnv  15807  bitsinv1  16388  smuval2  16428  firest  17371  sscres  17761  funcres2c  17841  coffth  17876  rescfth  17877  catcoppccl  18055  catcfuccl  18056  catcxpccl  18144  psssdm2  18516  sylow2a  19525  frgpnabllem2  19780  idomdomd  20611  sralmod  21070  2idlridld  21141  zringlpirlem3  21350  mplind  21953  neiptoptop  22994  restbas  23021  ordtrest  23065  subbascn  23117  lmss  23161  cnconn  23285  clsconn  23293  conncompclo  23298  subislly  23344  cldllycmp  23358  1stckgenlem  23416  txcls  23467  txcnp  23483  txtube  23503  txcmplem1  23504  txkgen  23515  xkopt  23518  xkococnlem  23522  txconn  23552  basqtop  23574  tgqtop  23575  kqnrmlem1  23606  kqnrmlem2  23607  nrmhmph  23657  uzrest  23760  alexsubALTlem3  23912  ptcmplem2  23916  tsmslem1  23992  tsmsxplem1  24016  tsmsxplem2  24017  tsmsxp  24018  blin2  24293  met2ndci  24386  zdis  24681  reconnlem2  24692  reconn  24693  xrge0gsumle  24698  cnheibor  24830  lebnum  24839  nmoleub2lem3  24991  nmoleub3  24995  caussi  25173  minveclem4b  25307  minveclem4  25308  ovolfcl  25343  ovolfioo  25344  ovolficc  25345  ovolficcss  25346  ovolfsval  25347  ovoliunlem1  25379  ovolicc2lem4  25397  ovolicc2lem5  25398  uniiccdif  25455  uniioovol  25456  uniiccvol  25457  uniioombllem2a  25459  uniioombllem3a  25461  uniioombllem4  25463  uniioombllem5  25464  uniioombllem6  25465  vitalilem2  25486  vitalilem4  25488  ig1peu  26056  taylfvallem1  26240  tayl0  26245  ppisval  26990  chtf  26994  efchtcl  26997  chtge0  26998  ppinprm  27038  chtprm  27039  chtnprm  27040  chtwordi  27042  chtdif  27044  efchtdvds  27045  chtlepsi  27093  chtleppi  27097  pclogsum  27102  chpval2  27105  chpchtsum  27106  chpub  27107  chebbnd1lem1  27356  chtppilimlem1  27360  rplogsumlem2  27372  perpneq  28617  ragperp  28620  tocyc01  33048  cyc3evpm  33080  cycpmconjslem2  33085  cyc3conja  33087  ssdifidlprm  33402  mxidlirred  33416  pidufd  33487  1arithufdlem4  33491  ressdeg1  33508  exsslsb  33565  lbsdiflsp0  33595  irngss  33655  rtelextdg2lem  33689  esum2d  34056  ispisys2  34116  sigapisys  34118  sigapildsyslem  34124  sigapildsys  34125  sseqf  34356  tgoldbachgt  34627  bnj1172  34964  weiunfrlem  36425  mhpind  42555  ismnushort  44263  cnrefiisplem  45800  hoiqssbllem3  46595  smflimlem3  46744  iinfconstbas  49028  ffthoppf  49127  fucoppc  49372  termcterm  49475  termcterm2  49476