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

Theorem ssexg 3716
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 2833 . . . 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 2475 . . . 4  |-  x  e. 
_V
43ssex 3714 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2523 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 415 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 356    = wceq 1517    e. wcel 1519   _Vcvv 2472    C_ wss 2790
This theorem is referenced by:  difexg  3717  rabexg  3719  elssabg  3721  elpw2g  3722  abssexg  3748  snexALT  3749  sess1  3908  sess2  3909  trsuc  4023  ordsssuc2  4028  unexb  4065  difex2  4070  uniexb  4126  xpexg  4378  riinint  4512  dmexg  4516  rnexg  4517  resexg  4571  resiexg  4574  imaexg  4602  exse2  4623  soex  4698  cnvexg  4781  coexg  4788  fex2  4924  fabexg  4944  f1oabexg  5003  resfunexgALT  5180  cofunexg  5181  fnexALT  5184  mptexg  5187  f1dmex  5193  isofr2  5339  oprabexd  5448  mpt2exg  5450  ofres  5579  fnwelem  5707  fnse  5709  tposexg  5723  brrpssg  5750  tz7.48-3  5903  oaabs  6089  erex  6131  mapex  6215  pmvalg  6220  elpmg  6223  pmss12g  6231  ixpexg  6271  ssdomg  6337  f1imaen2g  6351  fiprc  6371  domunsncan  6391  infensuc  6515  pssnn  6554  unbnn  6586  fodomfi  6608  fival  6638  fiss  6649  dffi3  6656  ordtypelem10  6715  oismo  6728  hartogslem2  6731  wofib  6733  wemapso  6739  card2on  6741  wdom2d  6767  wdomd  6768  wdomima2g  6773  unxpwdom2  6775  unxpwdom  6776  harwdom  6777  cantnfle  6845  cantnflt  6846  cantnflt2  6847  cantnfp1lem2  6854  cantnfp1lem3  6855  oemapvali  6859  cantnflem1b  6861  cantnflem1d  6863  cantnflem1  6864  cnfcomlem  6875  cnfcom  6876  cnfcom2lem  6877  cnfcom3lem  6879  acni2  7145  ackbij1lem11  7309  cofsmo  7348  ssfin4  7389  fin23lem11  7396  ssfin2  7399  ssfin3ds  7409  isfin1-3  7465  fin1a2lem12  7490  hsmexlem1  7505  hsmex3  7513  axdc2lem  7527  ac6num  7554  zorn2lem1  7589  zorn2lem4  7592  ttukeylem1  7602  ondomon  7649  fpwwe2lem2  7716  fpwwe2lem3  7717  fpwwe2lem5  7718  fpwwe2lem12  7725  fpwwe2lem13  7726  fpwwe2  7727  fpwwelem  7729  canthwelem  7734  canthwe  7735  pwfseqlem4  7745  genpv  8033  genpdm  8036  hashf1lem1  10330  shftfval  10344  o1of2  10713  o1rlimmul  10718  isercolllem2  10749  hashbcss  11534  isstruct2  11639  strssd  11660  ressabs  11683  restid2  11801  prdsbas  11821  divsfval  11911  ipolerval  12145  wrdexg  12333  wrdexb  12357  gass  12763  symgbas  12780  sylow2a  12863  sylow2blem2  12865  islbs3  13677  mplsubglem  13944  mpllsslem  13945  opsrtoslem2  13991  fnmrc  14406  mrcfval  14407  isacs1i  14441  mreacs  14442  istps3OLD  14494  basdif0  14525  tgval  14527  eltg  14529  eltg2  14530  tgss  14540  basgen2  14561  2basgen  14562  tgdif0  14564  bastop1  14565  resttopon  14703  restabs  14707  restcld  14714  restfpw  14721  restcls  14722  restntr  14723  lpval  14729  ordtbaslem  14737  ordtbas2  14740  ordtbas  14741  ordtrest2  14753  lmfval  14781  cnrest  14832  cnrest2  14833  cnpresti  14835  cnprest  14836  cnprest2  14837  cmpcov  14932  cmpsublem  14942  cmpsub  14943  consuba  14962  consubclo  14966  uncon  14971  2ndcomap  14999  1stcelcls  15002  hausmapdom  15041  ptbasfi  15091  txss12  15115  ptcls  15125  ptrescn  15148  cnmpt2res  15186  qtopval2  15202  elqtop  15203  qtoprest  15223  ptuncnv  15313  ptunhmeo  15314  trfbas2  15353  trfbas  15354  isfildlem  15367  snfbas  15376  fsubbas  15377  trfil1  15396  trfil2  15397  trufil  15420  ssufl  15428  elfm  15457  rnelfmlem  15462  rnelfm  15463  fmfnfmlem4  15467  flimclslem  15494  hauspwpwf1  15497  hauspwpwdom  15498  ptcmplem1  15561  xmetres2  15740  metrest  15886  cnheibor  16262  fmcfil  16505  metcld2  16539  bcthlem1  16553  mbfimaopn2  16819  0pledm  16835  dvfval  17027  dvbss  17032  dvlmlem1  17034  dvlmlem2  17035  dvlm  17036  dvreslem  17043  dvres2lem  17044  dvcnp2  17053  dvnf  17059  dvnbss  17060  dvaddbr  17069  dvmulbr  17070  dvaddf  17073  dvmulf  17074  dvcmulf  17076  dvcof  17079  dvcnvrelem2  17131  elply2  17327  plyf  17329  plyss  17330  elplyr  17332  plyeq0lem  17341  plyeq0  17342  plyaddlem  17346  plymullem  17347  dgrlem  17360  coeidlem  17368  ulmss  17468  ulmcn  17470  pserulm  17492  issubgo  18286  erdsze2lem1  20391  erdsze2lem2  20392  cvxpcon  20430  cvmliftmolem1  20469  iseupa  20538  dfon2lem3  20815  setlikess  20871  altxpexg  21193  oprabex2gpop  21653  sndw  21717  prjmapcp  21785  prjmapcp2  21790  ubpar  21881  qusp  22168  efilcp  22178  cnfilca  22182  islimrs3  22207  islimrs4  22208  fnctartar3  22535  prismorcsetlem  22538  prismorcset  22540  lemindclsbu  22682  indcls2  22683  ivthALT  22802  islocfin  22840  neibastop2lem  22853  fnejoin1  22861  filnetlem3  22873  filnetlem4  22874  abrexdom  22950  sdclem2  22997  sdclem1  22998  ralxpmap  23308  elrfi  23316  elrfirn  23317  elrfirn2  23318  elmapssres  23339  pwssplit0  23811  pwssplit1  23812  pwssplit2  23813  pwssplit3  23814  pwssplit4  23815  frlmsplit2  23867  frlmsslss  23868  hbtlem1  23951  hbtlem7  23953  pmtrfconj  24031  bnj74  25151  bnj1412  26222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-sep 3697
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1444  df-sb 1733  df-clab 2049  df-cleq 2054  df-clel 2057  df-v 2474  df-in 2797  df-ss 2801
Copyright terms: Public domain