Theorem elin2d 4134

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

Syntax hints:   → wi 4   ∈ wcel 2119   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  f1opwfi  9256  elfiun  9333  ordtypelem3  9425  infpwfien  9975  ttukeylem6  10427  fpwwe2lem11  10555  explecnv  15821  bitsinv1  16402  smuval2  16442  firest  17386  sscres  17781  funcres2c  17861  coffth  17896  rescfth  17897  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  psssdm2  18538  sylow2a  19585  frgpnabllem2  19840  idomdomd  20698  sralmod  21177  2idlridld  21248  zringlpirlem3  21439  mplind  22046  neiptoptop  23114  restbas  23141  ordtrest  23185  subbascn  23237  lmss  23281  cnconn  23405  clsconn  23413  conncompclo  23418  subislly  23464  cldllycmp  23478  1stckgenlem  23536  txcls  23587  txcnp  23603  txtube  23623  txcmplem1  23624  txkgen  23635  xkopt  23638  xkococnlem  23642  txconn  23672  basqtop  23694  tgqtop  23695  kqnrmlem1  23726  kqnrmlem2  23727  nrmhmph  23777  uzrest  23880  alexsubALTlem3  24032  ptcmplem2  24036  tsmslem1  24112  tsmsxplem1  24136  tsmsxplem2  24137  tsmsxp  24138  blin2  24412  met2ndci  24505  zdis  24800  reconnlem2  24811  reconn  24812  xrge0gsumle  24817  cnheibor  24940  lebnum  24949  nmoleub2lem3  25100  nmoleub3  25104  caussi  25282  minveclem4b  25416  minveclem4  25417  ovolfcl  25451  ovolfioo  25452  ovolficc  25453  ovolficcss  25454  ovolfsval  25455  ovoliunlem1  25487  ovolicc2lem4  25505  ovolicc2lem5  25506  uniiccdif  25563  uniioovol  25564  uniiccvol  25565  uniioombllem2a  25567  uniioombllem3a  25569  uniioombllem4  25571  uniioombllem5  25572  uniioombllem6  25573  vitalilem2  25594  vitalilem4  25596  ig1peu  26158  taylfvallem1  26340  tayl0  26345  ppisval  27085  chtf  27089  efchtcl  27092  chtge0  27093  ppinprm  27133  chtprm  27134  chtnprm  27135  chtwordi  27137  chtdif  27139  efchtdvds  27140  chtlepsi  27187  chtleppi  27191  pclogsum  27196  chpval2  27199  chpchtsum  27200  chpub  27201  chebbnd1lem1  27450  chtppilimlem1  27454  rplogsumlem2  27466  perpneq  28800  ragperp  28803  tocyc01  33199  cyc3evpm  33231  cycpmconjslem2  33236  cyc3conja  33238  ssdifidlprm  33541  mxidlirred  33555  pidufd  33626  1arithufdlem4  33630  ressdeg1  33649  exsslsb  33781  lbsdiflsp0  33810  irngss  33871  rtelextdg2lem  33910  esum2d  34277  ispisys2  34337  sigapisys  34339  sigapildsyslem  34345  sigapildsys  34346  sseqf  34576  tgoldbachgt  34847  bnj1172  35183  weiunfrlem  36692  dfttc4  36758  mhpind  43044  ismnushort  44745  cnrefiisplem  46272  hoiqssbllem3  47067  smflimlem3  47216  iinfconstbas  49556  ffthoppf  49655  fucoppc  49900  termcterm  50003  termcterm2  50004