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

Theorem ssexg 4160
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 sseq2 3200 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 308 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2791 . . . 4  |-  x  e. 
_V
43ssex 4158 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2843 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 419 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   _Vcvv 2788    C_ wss 3152
This theorem is referenced by:  ssexd  4161  difexg  4162  rabexg  4164  elssabg  4166  elpw2g  4174  abssexg  4195  snexALT  4196  sess1  4361  sess2  4362  trsuc  4476  ordsssuc2  4481  unexb  4520  difex2  4525  uniexb  4563  xpexg  4800  riinint  4935  dmexg  4939  rnexg  4940  resexg  4994  resiexg  4997  imaexg  5026  exse2  5047  soex  5122  cnvexg  5208  coexg  5215  fex2  5401  fabexg  5422  f1oabexg  5484  resfunexgALT  5738  cofunexg  5739  fnexALT  5742  mptexg  5745  f1dmex  5751  isofr2  5841  oprabexd  5960  ofres  6094  mpt2exxg  6195  fnwelem  6230  fnse  6232  tposexg  6248  brrpssg  6279  tz7.48-3  6456  oaabs  6642  erex  6684  mapex  6778  pmvalg  6783  elpmg  6786  pmss12g  6794  ixpexg  6840  ssdomg  6907  f1imaen2g  6922  fiprc  6942  domunsncan  6962  infensuc  7039  pssnn  7081  unbnn  7113  fodomfi  7135  fival  7166  fiss  7177  dffi3  7184  ordtypelem10  7242  oismo  7255  hartogslem2  7258  wofib  7260  wemapso  7266  card2on  7268  wdom2d  7294  wdomd  7295  wdomima2g  7300  unxpwdom2  7302  unxpwdom  7303  harwdom  7304  cantnfle  7372  cantnflt  7373  cantnflt2  7374  cantnfp1lem2  7381  cantnfp1lem3  7382  oemapvali  7386  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cnfcomlem  7402  cnfcom  7403  cnfcom2lem  7404  cnfcom3lem  7406  acni2  7673  ackbij1lem11  7856  cofsmo  7895  ssfin4  7936  fin23lem11  7943  ssfin2  7946  ssfin3ds  7956  isfin1-3  8012  fin1a2lem12  8037  hsmexlem1  8052  hsmex3  8060  axdc2lem  8074  ac6num  8106  zorn2lem1  8123  zorn2lem4  8126  ttukeylem1  8136  ondomon  8185  fpwwe2lem2  8254  fpwwe2lem3  8255  fpwwe2lem5  8256  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  fpwwelem  8267  canthwelem  8272  canthwe  8273  pwfseqlem4  8284  wuncss  8367  genpv  8623  genpdm  8626  hashf1lem1  11393  wrdexg  11425  wrdexb  11449  shftfval  11565  o1of2  12086  o1rlimmul  12092  isercolllem2  12139  hashbcss  13051  isstruct2  13157  strssd  13182  ressabs  13206  restid2  13335  prdsbas  13357  divsfval  13449  fnmrc  13509  mrcfval  13510  isacs1i  13559  mreacs  13560  isssc  13697  rescabs  13710  rescabs2  13711  resssetc  13924  resscatc  13937  yonedalem1  14046  yonedalem21  14047  yonedalem3a  14048  yonedalem4c  14051  yonedalem22  14052  yonedalem3b  14053  yonedainv  14055  yonffthlem  14056  ipolerval  14259  gass  14755  symgbas  14772  sylow2a  14930  sylow2blem2  14932  dprdres  15263  islbs3  15908  mplsubglem  16179  mpllsslem  16180  opsrtoslem2  16226  istps3OLD  16660  basdif0  16691  tgval  16693  eltg  16695  eltg2  16696  tgss  16706  basgen2  16727  2basgen  16728  tgdif0  16730  bastop1  16731  lpval  16871  resttopon  16892  restabs  16896  restcld  16903  restfpw  16910  restcls  16911  restntr  16912  ordtbaslem  16918  ordtbas2  16921  ordtbas  16922  ordtrest2  16934  lmfval  16962  cnrest  17013  cnrest2  17014  cnpresti  17016  cnprest  17017  cnprest2  17018  cmpcov  17116  cmpsublem  17126  cmpsub  17127  consuba  17146  consubclo  17150  uncon  17155  2ndcomap  17184  1stcelcls  17187  hausmapdom  17226  ptbasfi  17276  txss12  17300  ptcls  17310  ptrescn  17333  cnmpt2res  17371  qtopval2  17387  elqtop  17388  qtoprest  17408  ptuncnv  17498  ptunhmeo  17499  trfbas2  17538  trfbas  17539  isfildlem  17552  snfbas  17561  fsubbas  17562  trfil1  17581  trfil2  17582  trufil  17605  ssufl  17613  elfm  17642  rnelfmlem  17647  rnelfm  17648  fmfnfmlem4  17652  flimclslem  17679  hauspwpwf1  17682  hauspwpwdom  17683  ptcmplem1  17746  xmetres2  17925  metrest  18070  cnheibor  18453  fmcfil  18698  metcld2  18732  bcthlem1  18746  mbfimaopn2  19012  0pledm  19028  dvbss  19251  dvreslem  19259  dvres2lem  19260  dvcnp2  19269  dvnf  19276  dvnbss  19277  dvaddbr  19287  dvmulbr  19288  dvaddf  19291  dvmulf  19292  dvcmulf  19294  dvcof  19297  dvcnvrelem2  19365  elply2  19578  plyf  19580  plyss  19581  elplyr  19583  plyeq0lem  19592  plyeq0  19593  plyaddlem  19597  plymullem  19598  dgrlem  19611  coeidlem  19619  ulmss  19774  ulmcn  19776  pserulm  19798  issubgo  20970  abrexdomjm  23165  rabexgfGS  23171  dmct  23342  lmlim  23371  esumpinfval  23441  sigagenss  23510  measbase  23528  measval  23529  ismeas  23530  indval  23597  erdsze2lem1  23734  erdsze2lem2  23735  cvxpcon  23773  cvmliftmolem1  23812  iseupa  23881  dfon2lem3  24141  setlikess  24195  altxpexg  24512  oprabex2gpop  25036  sndw  25100  prjmapcp  25165  prjmapcp2  25170  ubpar  25261  qusp  25542  efilcp  25552  cnfilca  25556  islimrs3  25581  islimrs4  25582  fnctartar3  25909  prismorcsetlem  25912  prismorcset  25914  lemindclsbu  25995  indcls2  25996  ivthALT  26258  islocfin  26296  neibastop2lem  26309  fnejoin1  26317  filnetlem3  26329  filnetlem4  26330  abrexdom  26405  sdclem2  26452  sdclem1  26453  ralxpmap  26761  elrfi  26769  elrfirn  26770  elrfirn2  26771  elmapssres  26792  pwssplit0  27187  pwssplit1  27188  pwssplit2  27189  pwssplit3  27190  pwssplit4  27191  frlmsplit2  27243  frlmsslss  27244  hbtlem1  27327  hbtlem7  27329  pmtrfconj  27407  rabexgf  27695  stoweidlem31  27780  stoweidlem53  27802  stoweidlem57  27806  stoweidlem59  27808  bnj1413  29065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator