HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ssexg 3707
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized).
Assertion
Ref Expression
ssexg

Proof of Theorem ssexg
StepHypRef Expression
1 sseq2 2853 . . . 4
21imbi1d 306 . . 3
3 vex 2503 . . . 4
43ssex 3705 . . 3
52, 4vtoclg 2551 . 2
65impcom 415 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   wceq 1531   wcel 1533  cvv 2500   wss 2810
This theorem is referenced by:  difexg  3708  rabexg  3710  elssabg  3712  elpw2g  3713  abssexg  3739  snexALT  3740  sess1  3900  sess2  3901  trsuc  4015  ordsssuc2  4020  unexb  4057  difex2  4062  uniexb  4123  xpexg  4374  dmexg  4498  rnexg  4499  resexg  4550  resiexg  4553  imaexg  4578  exse2  4599  soex  4665  cnvexg  4739  coexg  4746  fex2  4878  fabexg  4898  f1oabexg  4957  resfunexgALT  5124  cofunexg  5125  fnexALT  5128  opabex2g  5132  f1dmex  5138  isofr2  5282  oprabexd  5367  oprabex2g  5369  ofres  5585  fnwelem  5722  fnse  5724  brrpssg  5728  tz7.48-3  5880  oaabs  6058  mapex  6175  pmvalg  6180  elpmg  6183  pmss12g  6190  ixpexg  6229  ssdomg  6292  f1imaen2g  6306  cnven  6320  fiprc  6326  domunsncan  6346  infensuc  6470  pssnn  6509  unbnn  6535  fodomfi  6560  fival  6583  fiss  6591  dffi3  6597  ordtypelem10  6656  oismo  6669  hartogslem2  6672  wofib  6674  wemapso  6680  card2on  6682  wdom2d  6708  wdomd  6709  wdomima2g  6714  unxpwdom2  6716  unxpwdom  6717  harwdom  6718  cantnfle  6785  cantnflt  6786  cantnflt2  6787  cantnfp1lem2  6794  cantnfp1lem3  6795  oemapvali  6799  cantnflem1b  6801  cantnflem1d  6803  cantnflem1  6804  cnfcomlem  6815  cnfcom  6816  cnfcom2lem  6817  cnfcom3lem  6819  fodomnumlem  7076  ackbij1lem11  7225  cofsmo  7264  ssfin4  7305  fin23lem11  7312  ssfin2  7315  ssfin3ds  7325  isfin1-3  7381  fin1a2lem12  7406  hsmexlem1  7421  hsmex3  7429  axdc2lem  7442  zorn2lem1  7504  zorn2lem4  7507  ttukeylem1  7517  ondomon  7562  fpwwe2lem2  7630  fpwwe2lem3  7631  fpwwe2lem5  7632  fpwwe2lem12  7639  fpwwe2lem13  7640  fpwwe2  7641  fpwwelem  7643  canthwelem  7648  canthwe  7649  pwfseqlem4  7659  genpv  7947  genpdm  7950  hashf1lem1  10054  shftfval  10067  o1of2  10431  o1rlimmul  10436  isercolllem2  10467  hashbcss  11249  strssd  11362  ressbas2  11376  ressabs  11383  divsfval  11532  ipolerval  11741  eqgfval  12044  gass  12120  symgbas  12137  sylow1lem3  12186  sylow2alem2  12202  sylow2a  12203  sylow2blem2  12205  gsumval  12275  gsumval3  12286  islbs3  12886  mplsubglem  13146  mpllsslem  13147  opsrtoslem2  13192  fnmrc  13447  mrcfval  13448  istps3OLD  13498  istps3  13503  tgval  13521  eltg  13523  eltg2  13524  tgss  13545  basgen2  13548  subtopbas  13554  restuni  13681  stoig  13682  restabs  13684  restcld  13690  restcls  13699  restntr  13700  lpval  13704  lmfval  13719  cnrest  13758  cnrest2  13759  cnpresti  13761  cnprest  13762  cnprest2  13763  cmpcov  13803  cmpsublem  13806  cmpsub  13807  consuba  13831  consubclo  13835  conima  13836  uncon  13840  2ndcomap  13867  1stcelcls  13906  hausmapdom  13907  1stckgenlem  13928  ptbasfi  13956  ptrescn  13989  cnmpt2res  14027  qtopval2  14041  elqtop  14042  qtoprest  14057  hmeofval  14064  hmeores  14072  ptuncnv  14080  ptunhmeo  14081  isfildlem  14117  snfbas  14126  fsubbas  14127  trfil1  14145  trfil2  14146  flimclslem  14196  hauspwpwf1  14198  hauspwpwdom  14199  elfm  14208  metrest  14330  cnmptre  14430  metcld2  14581  cmsss  14590  bcthlem1  14592  cncfmptc  14626  cncfcnvcn  14630  cnheibor  14633  mbfimaopn2  14840  cncombf  14841  0pledm  14856  dvvallem  15047  dvfval  15048  dvbss  15053  dvlmlem1  15055  dvlmlem2  15056  dvlm  15057  dvreslem  15064  dvres2lem  15065  dvcnp2  15074  dvcn  15075  dvnf  15080  dvnbss  15081  dvaddbr  15090  dvmulbr  15091  dvaddf  15094  dvmulf  15095  dvcmulf  15097  dvcobr  15098  dvcof  15100  dvcjbr  15101  dvmptntr  15121  dvcnvlem  15124  dvcnvrelem2  15152  dvcnvre  15153  ftc1lem3  15158  elply2  15348  plyf  15350  plyss  15351  elplyr  15353  plyeq0lem  15362  plyeq0  15363  plyaddlem  15367  plymullem  15368  dgrlem  15381  coeidlem  15389  ulmss  15489  ulmcn  15491  pserulm  15513  issubgo  16304  erdsze2lem1  18414  erdsze2lem2  18415  cvxpcon  18458  cvmliftmolem1  18497  cvmlift2lem9a  18519  cvmlift2lem9  18527  cvmlift3lem6  18540  cvmlift3lem7  18541  iseupa  18565  dfon2lem3  18825  setlikess  18883  altxpexg  19207  oprabex2gpop  19644  sndw  19722  prjmapcp  19793  prjmapcp2  19798  ubpar  19891  qusp  20213  efilcp  20223  cnfilca  20227  islimrs3  20252  islimrs4  20253  dualded  20488  dualcat2  20489  fnctartar3  20614  prismorcsetlem  20617  prismorcset  20619  isline1  20691  lemindclsbu  20736  indcls2  20737  cncls  20852  ivthALT  20866  topjoin  20923  fnejoin1  20926  rnelfmlem  20964  rnelfm  20965  fmfnfmlem4  20969  filnetlem3  21014  filnetlem4  21015  abrexdom  21092  sdclem2  21141  sdclem1  21142  cnres2  21172  cnresima  21173  sstotbnd  21187  totbndss  21188  ismtyval  21198  erex  21414  ralxpmap  21449  riinint  21467  elrfi  21475  elrfirn  21476  elrfirn2  21477  isacs1i  21510  mreacs  21511  elmapssres  21535  pwssplit0  22009  pwssplit1  22010  pwssplit2  22011  pwssplit3  22012  pwssplit4  22013  frlmsplit2  22065  frlmsslss  22066  islinds2  22105  hbtlem1  22149  hbtlem7  22151  bnj74  23166  bnj1412  24237
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1451  df-sb 1751  df-clab 2078  df-cleq 2083  df-clel 2086  df-v 2502  df-in 2817  df-ss 2821
Copyright terms: Public domain