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

Theorem ssexg 3720
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 2836 . . . 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 2478 . . . 4  |-  x  e. 
_V
43ssex 3718 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2526 . 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 2475    C_ wss 2793
This theorem is referenced by:  difexg  3721  rabexg  3723  elssabg  3725  elpw2g  3726  abssexg  3752  snexALT  3753  sess1  3912  sess2  3913  trsuc  4027  ordsssuc2  4032  unexb  4069  difex2  4074  uniexb  4130  xpexg  4382  riinint  4517  dmexg  4521  rnexg  4522  resexg  4576  resiexg  4579  imaexg  4607  exse2  4628  soex  4703  cnvexg  4786  coexg  4793  fex2  4929  fabexg  4950  f1oabexg  5009  resfunexgALT  5187  cofunexg  5188  fnexALT  5191  mptexg  5194  f1dmex  5200  isofr2  5346  oprabexd  5455  mpt2exg  5457  ofres  5586  fnwelem  5715  fnse  5717  tposexg  5731  brrpssg  5758  tz7.48-3  5911  oaabs  6097  erex  6139  mapex  6223  pmvalg  6228  elpmg  6231  pmss12g  6239  ixpexg  6279  ssdomg  6345  f1imaen2g  6359  fiprc  6379  domunsncan  6399  infensuc  6523  pssnn  6564  unbnn  6596  fodomfi  6618  fival  6648  fiss  6659  dffi3  6666  ordtypelem10  6725  oismo  6738  hartogslem2  6741  wofib  6743  wemapso  6749  card2on  6751  wdom2d  6777  wdomd  6778  wdomima2g  6783  unxpwdom2  6785  unxpwdom  6786  harwdom  6787  cantnfle  6855  cantnflt  6856  cantnflt2  6857  cantnfp1lem2  6864  cantnfp1lem3  6865  oemapvali  6869  cantnflem1b  6871  cantnflem1d  6873  cantnflem1  6874  cnfcomlem  6885  cnfcom  6886  cnfcom2lem  6887  cnfcom3lem  6889  acni2  7155  ackbij1lem11  7319  cofsmo  7358  ssfin4  7399  fin23lem11  7406  ssfin2  7409  ssfin3ds  7419  isfin1-3  7475  fin1a2lem12  7500  hsmexlem1  7515  hsmex3  7523  axdc2lem  7537  ac6num  7564  zorn2lem1  7599  zorn2lem4  7602  ttukeylem1  7612  ondomon  7659  fpwwe2lem2  7726  fpwwe2lem3  7727  fpwwe2lem5  7728  fpwwe2lem12  7735  fpwwe2lem13  7736  fpwwe2  7737  fpwwelem  7739  canthwelem  7744  canthwe  7745  pwfseqlem4  7756  genpv  8044  genpdm  8047  hashf1lem1  10746  shftfval  10760  o1of2  11277  o1rlimmul  11283  isercolllem2  11330  hashbcss  12156  isstruct2  12261  strssd  12282  ressabs  12305  restid2  12423  prdsbas  12443  divsfval  12533  fnmrc  12591  mrcfval  12592  isacs1i  12613  mreacs  12614  ipolerval  12819  wrdexg  13024  wrdexb  13048  gass  13464  symgbas  13481  sylow2a  13639  sylow2blem2  13641  dprdres  13971  islbs3  14615  mplsubglem  14885  mpllsslem  14886  opsrtoslem2  14932  istps3OLD  15366  basdif0  15397  tgval  15399  eltg  15401  eltg2  15402  tgss  15412  basgen2  15433  2basgen  15434  tgdif0  15436  bastop1  15437  resttopon  15575  restabs  15579  restcld  15586  restfpw  15593  restcls  15594  restntr  15595  lpval  15601  ordtbaslem  15609  ordtbas2  15612  ordtbas  15613  ordtrest2  15625  lmfval  15653  cnrest  15704  cnrest2  15705  cnpresti  15707  cnprest  15708  cnprest2  15709  cmpcov  15804  cmpsublem  15814  cmpsub  15815  consuba  15834  consubclo  15838  uncon  15843  2ndcomap  15871  1stcelcls  15874  hausmapdom  15913  ptbasfi  15963  txss12  15987  ptcls  15997  ptrescn  16020  cnmpt2res  16058  qtopval2  16074  elqtop  16075  qtoprest  16095  ptuncnv  16185  ptunhmeo  16186  trfbas2  16225  trfbas  16226  isfildlem  16239  snfbas  16248  fsubbas  16249  trfil1  16268  trfil2  16269  trufil  16292  ssufl  16300  elfm  16329  rnelfmlem  16334  rnelfm  16335  fmfnfmlem4  16339  flimclslem  16366  hauspwpwf1  16369  hauspwpwdom  16370  ptcmplem1  16433  xmetres2  16612  metrest  16758  cnheibor  17135  fmcfil  17378  metcld2  17412  bcthlem1  17426  mbfimaopn2  17692  0pledm  17708  dvfval  17900  dvbss  17905  dvlmlem1  17907  dvlmlem2  17908  dvlm  17909  dvreslem  17916  dvres2lem  17917  dvcnp2  17926  dvnf  17932  dvnbss  17933  dvaddbr  17942  dvmulbr  17943  dvaddf  17946  dvmulf  17947  dvcmulf  17949  dvcof  17952  dvcnvrelem2  18010  elply2  18221  plyf  18223  plyss  18224  elplyr  18226  plyeq0lem  18235  plyeq0  18236  plyaddlem  18240  plymullem  18241  dgrlem  18254  coeidlem  18262  ulmss  18362  ulmcn  18364  pserulm  18386  issubgo  19503  erdsze2lem1  21608  erdsze2lem2  21609  cvxpcon  21647  cvmliftmolem1  21686  iseupa  21755  dfon2lem3  22011  setlikess  22067  altxpexg  22389  oprabex2gpop  22851  sndw  22915  prjmapcp  22982  prjmapcp2  22987  ubpar  23078  qusp  23365  efilcp  23375  cnfilca  23379  islimrs3  23404  islimrs4  23405  fnctartar3  23732  prismorcsetlem  23735  prismorcset  23737  lemindclsbu  23816  indcls2  23817  ivthALT  24032  islocfin  24070  neibastop2lem  24083  fnejoin1  24091  filnetlem3  24103  filnetlem4  24104  abrexdom  24180  sdclem2  24227  sdclem1  24228  ralxpmap  24538  elrfi  24546  elrfirn  24547  elrfirn2  24548  elmapssres  24569  pwssplit0  25004  pwssplit1  25005  pwssplit2  25006  pwssplit3  25007  pwssplit4  25008  frlmsplit2  25060  frlmsslss  25061  hbtlem1  25144  hbtlem7  25146  pmtrfconj  25224  bnj74  26317  bnj1412  27388
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 1562  ax-10 1576  ax-9 1582  ax-4 1589  ax-16 1775  ax-ext 2046  ax-sep 3701
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1447  df-sb 1736  df-clab 2052  df-cleq 2057  df-clel 2060  df-v 2477  df-in 2800  df-ss 2804
Copyright terms: Public domain