MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssexg Unicode version

Theorem ssexg 4054
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 3118 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 310 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2728 . . . 4  |-  x  e. 
_V
43ssex 4052 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2779 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 421 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621   _Vcvv 2725    C_ wss 3075
This theorem is referenced by:  difexg  4055  rabexg  4057  elssabg  4059  elpw2g  4060  abssexg  4086  snexALT  4087  sess1  4251  sess2  4252  trsuc  4366  ordsssuc2  4371  unexb  4408  difex2  4413  uniexb  4451  xpexg  4704  riinint  4839  dmexg  4843  rnexg  4844  resexg  4898  resiexg  4901  imaexg  4930  exse2  4951  soex  5026  cnvexg  5111  coexg  5118  fex2  5255  fabexg  5276  f1oabexg  5338  resfunexgALT  5587  cofunexg  5588  fnexALT  5591  mptexg  5594  f1dmex  5600  isofr2  5690  oprabexd  5809  ofres  5943  mpt2exxg  6044  fnwelem  6079  fnse  6081  tposexg  6097  brrpssg  6128  tz7.48-3  6339  oaabs  6525  erex  6567  mapex  6661  pmvalg  6666  elpmg  6669  pmss12g  6677  ixpexg  6723  ssdomg  6790  f1imaen2g  6804  fiprc  6824  domunsncan  6844  infensuc  6921  pssnn  6963  unbnn  6995  fodomfi  7017  fival  7047  fiss  7058  dffi3  7065  ordtypelem10  7123  oismo  7136  hartogslem2  7139  wofib  7141  wemapso  7147  card2on  7149  wdom2d  7175  wdomd  7176  wdomima2g  7181  unxpwdom2  7183  unxpwdom  7184  harwdom  7185  cantnfle  7253  cantnflt  7254  cantnflt2  7255  cantnfp1lem2  7262  cantnfp1lem3  7263  oemapvali  7267  cantnflem1b  7269  cantnflem1d  7271  cantnflem1  7272  cnfcomlem  7283  cnfcom  7284  cnfcom2lem  7285  cnfcom3lem  7287  acni2  7554  ackbij1lem11  7737  cofsmo  7776  ssfin4  7817  fin23lem11  7824  ssfin2  7827  ssfin3ds  7837  isfin1-3  7893  fin1a2lem12  7918  hsmexlem1  7933  hsmex3  7941  axdc2lem  7955  ac6num  7987  zorn2lem1  8004  zorn2lem4  8007  ttukeylem1  8017  ondomon  8064  fpwwe2lem2  8131  fpwwe2lem3  8132  fpwwe2lem5  8133  fpwwe2lem12  8140  fpwwe2lem13  8141  fpwwe2  8142  fpwwelem  8144  canthwelem  8149  canthwe  8150  pwfseqlem4  8161  wuncss  8244  genpv  8500  genpdm  8503  hashf1lem1  11234  wrdexg  11266  wrdexb  11290  shftfval  11406  o1of2  11925  o1rlimmul  11931  isercolllem2  11978  hashbcss  12887  isstruct2  12993  strssd  13018  ressabs  13042  restid2  13171  prdsbas  13193  divsfval  13285  fnmrc  13343  mrcfval  13344  isacs1i  13365  mreacs  13366  isssc  13503  rescabs  13516  rescabs2  13517  resssetc  13730  resscatc  13743  yonedalem1  13852  yonedalem21  13853  yonedalem3a  13854  yonedalem4c  13857  yonedalem22  13858  yonedalem3b  13859  yonedainv  13861  yonffthlem  13862  ipolerval  14065  gass  14552  symgbas  14569  sylow2a  14727  sylow2blem2  14729  dprdres  15060  islbs3  15704  mplsubglem  15973  mpllsslem  15974  opsrtoslem2  16020  istps3OLD  16454  basdif0  16485  tgval  16487  eltg  16489  eltg2  16490  tgss  16500  basgen2  16521  2basgen  16522  tgdif0  16524  bastop1  16525  lpval  16665  resttopon  16686  restabs  16690  restcld  16697  restfpw  16704  restcls  16705  restntr  16706  ordtbaslem  16712  ordtbas2  16715  ordtbas  16716  ordtrest2  16728  lmfval  16756  cnrest  16807  cnrest2  16808  cnpresti  16810  cnprest  16811  cnprest2  16812  cmpcov  16910  cmpsublem  16920  cmpsub  16921  consuba  16940  consubclo  16944  uncon  16949  2ndcomap  16978  1stcelcls  16981  hausmapdom  17020  ptbasfi  17070  txss12  17094  ptcls  17104  ptrescn  17127  cnmpt2res  17165  qtopval2  17181  elqtop  17182  qtoprest  17202  ptuncnv  17292  ptunhmeo  17293  trfbas2  17332  trfbas  17333  isfildlem  17346  snfbas  17355  fsubbas  17356  trfil1  17375  trfil2  17376  trufil  17399  ssufl  17407  elfm  17436  rnelfmlem  17441  rnelfm  17442  fmfnfmlem4  17446  flimclslem  17473  hauspwpwf1  17476  hauspwpwdom  17477  ptcmplem1  17540  xmetres2  17719  metrest  17864  cnheibor  18247  fmcfil  18492  metcld2  18526  bcthlem1  18540  mbfimaopn2  18806  0pledm  18822  dvbss  19045  dvreslem  19053  dvres2lem  19054  dvcnp2  19063  dvnf  19070  dvnbss  19071  dvaddbr  19081  dvmulbr  19082  dvaddf  19085  dvmulf  19086  dvcmulf  19088  dvcof  19091  dvcnvrelem2  19159  elply2  19372  plyf  19374  plyss  19375  elplyr  19377  plyeq0lem  19386  plyeq0  19387  plyaddlem  19391  plymullem  19392  dgrlem  19405  coeidlem  19413  ulmss  19568  ulmcn  19570  pserulm  19592  issubgo  20731  erdsze2lem1  22836  erdsze2lem2  22837  cvxpcon  22875  cvmliftmolem1  22914  iseupa  22983  dfon2lem3  23240  setlikess  23294  altxpexg  23617  oprabex2gpop  24132  sndw  24196  prjmapcp  24262  prjmapcp2  24267  ubpar  24358  qusp  24639  efilcp  24649  cnfilca  24653  islimrs3  24678  islimrs4  24679  fnctartar3  25006  prismorcsetlem  25009  prismorcset  25011  lemindclsbu  25092  indcls2  25093  ivthALT  25355  islocfin  25393  neibastop2lem  25406  fnejoin1  25414  filnetlem3  25426  filnetlem4  25427  abrexdom  25502  sdclem2  25549  sdclem1  25550  ralxpmap  25858  elrfi  25866  elrfirn  25867  elrfirn2  25868  elmapssres  25889  pwssplit0  26284  pwssplit1  26285  pwssplit2  26286  pwssplit3  26287  pwssplit4  26288  frlmsplit2  26340  frlmsslss  26341  hbtlem1  26424  hbtlem7  26426  pmtrfconj  26504  bnj1413  27629
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4035
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2727  df-in 3082  df-ss 3086
  Copyright terms: Public domain W3C validator