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

Theorem ssexg 3726
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
ssexg  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )

Proof of Theorem ssexg
StepHypRef Expression
1 sseq2 2837 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 306 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2479 . . . 4  |-  x  e. 
_V
43ssex 3724 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2527 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 416 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 356    = wceq 1520    e. wcel 1522   _Vcvv 2476    C_ wss 2794
This theorem is referenced by:  difexg  3727  rabexg  3729  elssabg  3731  elpw2g  3732  abssexg  3758  snexALT  3759  sess1  3918  sess2  3919  trsuc  4033  ordsssuc2  4038  unexb  4075  difex2  4080  uniexb  4136  xpexg  4388  riinint  4523  dmexg  4527  rnexg  4528  resexg  4582  resiexg  4585  imaexg  4613  exse2  4634  soex  4709  cnvexg  4792  coexg  4799  fex2  4935  fabexg  4956  f1oabexg  5015  resfunexgALT  5193  cofunexg  5194  fnexALT  5197  mptexg  5200  f1dmex  5206  isofr2  5352  oprabexd  5461  mpt2exg  5463  ofres  5592  fnwelem  5721  fnse  5723  tposexg  5737  brrpssg  5764  tz7.48-3  5917  oaabs  6103  erex  6145  mapex  6229  pmvalg  6234  elpmg  6237  pmss12g  6245  ixpexg  6285  ssdomg  6351  f1imaen2g  6365  fiprc  6385  domunsncan  6405  infensuc  6529  pssnn  6570  unbnn  6602  fodomfi  6624  fival  6654  fiss  6665  dffi3  6672  ordtypelem10  6731  oismo  6744  hartogslem2  6747  wofib  6749  wemapso  6755  card2on  6757  wdom2d  6783  wdomd  6784  wdomima2g  6789  unxpwdom2  6791  unxpwdom  6792  harwdom  6793  cantnfle  6861  cantnflt  6862  cantnflt2  6863  cantnfp1lem2  6870  cantnfp1lem3  6871  oemapvali  6875  cantnflem1b  6877  cantnflem1d  6879  cantnflem1  6880  cnfcomlem  6891  cnfcom  6892  cnfcom2lem  6893  cnfcom3lem  6895  acni2  7161  ackbij1lem11  7325  cofsmo  7364  ssfin4  7405  fin23lem11  7412  ssfin2  7415  ssfin3ds  7425  isfin1-3  7481  fin1a2lem12  7506  hsmexlem1  7521  hsmex3  7529  axdc2lem  7543  ac6num  7570  zorn2lem1  7605  zorn2lem4  7608  ttukeylem1  7618  ondomon  7665  fpwwe2lem2  7732  fpwwe2lem3  7733  fpwwe2lem5  7734  fpwwe2lem12  7741  fpwwe2lem13  7742  fpwwe2  7743  fpwwelem  7745  canthwelem  7750  canthwe  7751  pwfseqlem4  7762  genpv  8050  genpdm  8053  hashf1lem1  10761  shftfval  10775  o1of2  11293  o1rlimmul  11299  isercolllem2  11346  hashbcss  12172  isstruct2  12277  strssd  12298  ressabs  12322  restid2  12440  prdsbas  12460  divsfval  12550  fnmrc  12608  mrcfval  12609  isacs1i  12630  mreacs  12631  ipolerval  12836  wrdexg  13041  wrdexb  13065  gass  13481  symgbas  13498  sylow2a  13656  sylow2blem2  13658  dprdres  13988  islbs3  14632  mplsubglem  14902  mpllsslem  14903  opsrtoslem2  14949  istps3OLD  15383  basdif0  15414  tgval  15416  eltg  15418  eltg2  15419  tgss  15429  basgen2  15450  2basgen  15451  tgdif0  15453  bastop1  15454  resttopon  15592  restabs  15596  restcld  15603  restfpw  15610  restcls  15611  restntr  15612  lpval  15618  ordtbaslem  15626  ordtbas2  15629  ordtbas  15630  ordtrest2  15642  lmfval  15670  cnrest  15721  cnrest2  15722  cnpresti  15724  cnprest  15725  cnprest2  15726  cmpcov  15821  cmpsublem  15831  cmpsub  15832  consuba  15851  consubclo  15855  uncon  15860  2ndcomap  15888  1stcelcls  15891  hausmapdom  15930  ptbasfi  15980  txss12  16004  ptcls  16014  ptrescn  16037  cnmpt2res  16075  qtopval2  16091  elqtop  16092  qtoprest  16112  ptuncnv  16202  ptunhmeo  16203  trfbas2  16242  trfbas  16243  isfildlem  16256  snfbas  16265  fsubbas  16266  trfil1  16285  trfil2  16286  trufil  16309  ssufl  16317  elfm  16346  rnelfmlem  16351  rnelfm  16352  fmfnfmlem4  16356  flimclslem  16383  hauspwpwf1  16386  hauspwpwdom  16387  ptcmplem1  16450  xmetres2  16629  metrest  16775  cnheibor  17152  fmcfil  17395  metcld2  17429  bcthlem1  17443  mbfimaopn2  17709  0pledm  17725  dvfval  17917  dvbss  17922  dvlmlem1  17924  dvlmlem2  17925  dvlm  17926  dvreslem  17933  dvres2lem  17934  dvcnp2  17943  dvnf  17949  dvnbss  17950  dvaddbr  17959  dvmulbr  17960  dvaddf  17963  dvmulf  17964  dvcmulf  17966  dvcof  17969  dvcnvrelem2  18027  elply2  18238  plyf  18240  plyss  18241  elplyr  18243  plyeq0lem  18252  plyeq0  18253  plyaddlem  18257  plymullem  18258  dgrlem  18271  coeidlem  18279  ulmss  18379  ulmcn  18381  pserulm  18403  issubgo  19522  erdsze2lem1  21627  erdsze2lem2  21628  cvxpcon  21666  cvmliftmolem1  21705  iseupa  21774  dfon2lem3  22028  setlikess  22084  altxpexg  22406  oprabex2gpop  22868  sndw  22932  prjmapcp  22999  prjmapcp2  23004  ubpar  23095  qusp  23382  efilcp  23392  cnfilca  23396  islimrs3  23421  islimrs4  23422  fnctartar3  23749  prismorcsetlem  23752  prismorcset  23754  lemindclsbu  23833  indcls2  23834  ivthALT  24049  islocfin  24087  neibastop2lem  24100  fnejoin1  24108  filnetlem3  24120  filnetlem4  24121  abrexdom  24197  sdclem2  24244  sdclem1  24245  ralxpmap  24555  elrfi  24563  elrfirn  24564  elrfirn2  24565  elmapssres  24586  pwssplit0  25021  pwssplit1  25022  pwssplit2  25023  pwssplit3  25024  pwssplit4  25025  frlmsplit2  25077  frlmsslss  25078  hbtlem1  25161  hbtlem7  25163  pmtrfconj  25241  bnj74  26342  bnj1412  27413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-17 1529  ax-12o 1563  ax-10 1577  ax-9 1583  ax-4 1590  ax-16 1776  ax-ext 2047  ax-sep 3707
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1447  df-sb 1737  df-clab 2053  df-cleq 2058  df-clel 2061  df-v 2478  df-in 2801  df-ss 2805
Copyright terms: Public domain