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

Theorem ssexg 3764
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 2873 . . . 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 2515 . . . 4  |-  x  e. 
_V
43ssex 3762 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2563 . 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 1531    e. wcel 1533   _Vcvv 2512    C_ wss 2830
This theorem is referenced by:  difexg  3765  rabexg  3767  elssabg  3769  elpw2g  3770  abssexg  3796  snexALT  3797  sess1  3956  sess2  3957  trsuc  4071  ordsssuc2  4076  unexb  4113  difex2  4118  uniexb  4174  xpexg  4426  riinint  4561  dmexg  4565  rnexg  4566  resexg  4620  resiexg  4623  imaexg  4651  exse2  4672  soex  4747  cnvexg  4830  coexg  4837  fex2  4973  fabexg  4994  f1oabexg  5053  resfunexgALT  5231  cofunexg  5232  fnexALT  5235  mptexg  5238  f1dmex  5244  isofr2  5390  oprabexd  5499  mpt2exg  5501  ofres  5630  fnwelem  5759  fnse  5761  tposexg  5775  brrpssg  5802  tz7.48-3  5955  oaabs  6141  erex  6183  mapex  6267  pmvalg  6272  elpmg  6275  pmss12g  6283  ixpexg  6323  ssdomg  6389  f1imaen2g  6403  fiprc  6423  domunsncan  6443  infensuc  6567  pssnn  6608  unbnn  6640  fodomfi  6662  fival  6692  fiss  6703  dffi3  6710  ordtypelem10  6769  oismo  6782  hartogslem2  6785  wofib  6787  wemapso  6793  card2on  6795  wdom2d  6821  wdomd  6822  wdomima2g  6827  unxpwdom2  6829  unxpwdom  6830  harwdom  6831  cantnfle  6899  cantnflt  6900  cantnflt2  6901  cantnfp1lem2  6908  cantnfp1lem3  6909  oemapvali  6913  cantnflem1b  6915  cantnflem1d  6917  cantnflem1  6918  cnfcomlem  6929  cnfcom  6930  cnfcom2lem  6931  cnfcom3lem  6933  acni2  7199  ackbij1lem11  7363  cofsmo  7402  ssfin4  7443  fin23lem11  7450  ssfin2  7453  ssfin3ds  7463  isfin1-3  7519  fin1a2lem12  7544  hsmexlem1  7559  hsmex3  7567  axdc2lem  7581  ac6num  7608  zorn2lem1  7643  zorn2lem4  7646  ttukeylem1  7656  ondomon  7703  fpwwe2lem2  7770  fpwwe2lem3  7771  fpwwe2lem5  7772  fpwwe2lem12  7779  fpwwe2lem13  7780  fpwwe2  7781  fpwwelem  7783  canthwelem  7788  canthwe  7789  pwfseqlem4  7800  genpv  8088  genpdm  8091  hashf1lem1  10799  shftfval  10813  o1of2  11331  o1rlimmul  11337  isercolllem2  11384  hashbcss  12210  isstruct2  12315  strssd  12336  ressabs  12360  restid2  12478  prdsbas  12498  divsfval  12588  fnmrc  12646  mrcfval  12647  isacs1i  12668  mreacs  12669  ipolerval  12874  wrdexg  13079  wrdexb  13103  gass  13519  symgbas  13536  sylow2a  13694  sylow2blem2  13696  dprdres  14026  islbs3  14670  mplsubglem  14940  mpllsslem  14941  opsrtoslem2  14987  istps3OLD  15421  basdif0  15452  tgval  15454  eltg  15456  eltg2  15457  tgss  15467  basgen2  15488  2basgen  15489  tgdif0  15491  bastop1  15492  resttopon  15630  restabs  15634  restcld  15641  restfpw  15648  restcls  15649  restntr  15650  lpval  15656  ordtbaslem  15664  ordtbas2  15667  ordtbas  15668  ordtrest2  15680  lmfval  15708  cnrest  15759  cnrest2  15760  cnpresti  15762  cnprest  15763  cnprest2  15764  cmpcov  15859  cmpsublem  15869  cmpsub  15870  consuba  15889  consubclo  15893  uncon  15898  2ndcomap  15926  1stcelcls  15929  hausmapdom  15968  ptbasfi  16018  txss12  16042  ptcls  16052  ptrescn  16075  cnmpt2res  16113  qtopval2  16129  elqtop  16130  qtoprest  16150  ptuncnv  16240  ptunhmeo  16241  trfbas2  16280  trfbas  16281  isfildlem  16294  snfbas  16303  fsubbas  16304  trfil1  16323  trfil2  16324  trufil  16347  ssufl  16355  elfm  16384  rnelfmlem  16389  rnelfm  16390  fmfnfmlem4  16394  flimclslem  16421  hauspwpwf1  16424  hauspwpwdom  16425  ptcmplem1  16488  xmetres2  16667  metrest  16813  cnheibor  17190  fmcfil  17433  metcld2  17467  bcthlem1  17481  mbfimaopn2  17747  0pledm  17763  dvfval  17955  dvbss  17960  dvlmlem1  17962  dvlmlem2  17963  dvlm  17964  dvreslem  17971  dvres2lem  17972  dvcnp2  17981  dvnf  17987  dvnbss  17988  dvaddbr  17997  dvmulbr  17998  dvaddf  18001  dvmulf  18002  dvcmulf  18004  dvcof  18007  dvcnvrelem2  18065  elply2  18276  plyf  18278  plyss  18279  elplyr  18281  plyeq0lem  18290  plyeq0  18291  plyaddlem  18295  plymullem  18296  dgrlem  18309  coeidlem  18317  ulmss  18417  ulmcn  18419  pserulm  18441  issubgo  19560  erdsze2lem1  21665  erdsze2lem2  21666  cvxpcon  21704  cvmliftmolem1  21743  iseupa  21812  dfon2lem3  22066  setlikess  22122  altxpexg  22444  oprabex2gpop  22916  sndw  22980  prjmapcp  23048  prjmapcp2  23053  ubpar  23144  qusp  23431  efilcp  23441  cnfilca  23445  islimrs3  23470  islimrs4  23471  fnctartar3  23798  prismorcsetlem  23801  prismorcset  23803  lemindclsbu  23885  indcls2  23886  ivthALT  24150  islocfin  24188  neibastop2lem  24201  fnejoin1  24209  filnetlem3  24221  filnetlem4  24222  abrexdom  24298  sdclem2  24345  sdclem1  24346  ralxpmap  24656  elrfi  24664  elrfirn  24665  elrfirn2  24666  elmapssres  24687  pwssplit0  25122  pwssplit1  25123  pwssplit2  25124  pwssplit3  25125  pwssplit4  25126  frlmsplit2  25178  frlmsslss  25179  hbtlem1  25262  hbtlem7  25264  pmtrfconj  25342  bnj1413  26468
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1452  ax-6 1453  ax-7 1454  ax-gen 1455  ax-8 1535  ax-11 1536  ax-17 1540  ax-12o 1574  ax-10 1588  ax-9 1594  ax-4 1601  ax-16 1787  ax-ext 2082  ax-sep 3745
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1457  df-sb 1748  df-clab 2088  df-cleq 2093  df-clel 2096  df-v 2514  df-in 2837  df-ss 2841
  Copyright terms: Public domain W3C validator