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

Theorem ssexg 4161
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 )
Dummy variable  x is distinct from all other variables.

Proof of Theorem ssexg
StepHypRef Expression
1 sseq2 3201 . . . 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 2792 . . . 4  |-  x  e. 
_V
43ssex 4159 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2844 . 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 1624    e. wcel 1685   _Vcvv 2789    C_ wss 3153
This theorem is referenced by:  ssexd  4162  difexg  4163  rabexg  4165  elssabg  4167  elpw2g  4168  abssexg  4194  snexALT  4195  sess1  4360  sess2  4361  trsuc  4475  ordsssuc2  4480  unexb  4519  difex2  4524  uniexb  4562  xpexg  4799  riinint  4934  dmexg  4938  rnexg  4939  resexg  4993  resiexg  4996  imaexg  5025  exse2  5046  soex  5121  cnvexg  5206  coexg  5213  fex2  5366  fabexg  5387  f1oabexg  5449  resfunexgALT  5699  cofunexg  5700  fnexALT  5703  mptexg  5706  f1dmex  5712  isofr2  5802  oprabexd  5921  ofres  6055  mpt2exxg  6156  fnwelem  6191  fnse  6193  tposexg  6209  brrpssg  6240  tz7.48-3  6451  oaabs  6637  erex  6679  mapex  6773  pmvalg  6778  elpmg  6781  pmss12g  6789  ixpexg  6835  ssdomg  6902  f1imaen2g  6917  fiprc  6937  domunsncan  6957  infensuc  7034  pssnn  7076  unbnn  7108  fodomfi  7130  fival  7161  fiss  7172  dffi3  7179  ordtypelem10  7237  oismo  7250  hartogslem2  7253  wofib  7255  wemapso  7261  card2on  7263  wdom2d  7289  wdomd  7290  wdomima2g  7295  unxpwdom2  7297  unxpwdom  7298  harwdom  7299  cantnfle  7367  cantnflt  7368  cantnflt2  7369  cantnfp1lem2  7376  cantnfp1lem3  7377  oemapvali  7381  cantnflem1b  7383  cantnflem1d  7385  cantnflem1  7386  cnfcomlem  7397  cnfcom  7398  cnfcom2lem  7399  cnfcom3lem  7401  acni2  7668  ackbij1lem11  7851  cofsmo  7890  ssfin4  7931  fin23lem11  7938  ssfin2  7941  ssfin3ds  7951  isfin1-3  8007  fin1a2lem12  8032  hsmexlem1  8047  hsmex3  8055  axdc2lem  8069  ac6num  8101  zorn2lem1  8118  zorn2lem4  8121  ttukeylem1  8131  ondomon  8180  fpwwe2lem2  8249  fpwwe2lem3  8250  fpwwe2lem5  8251  fpwwe2lem12  8258  fpwwe2lem13  8259  fpwwe2  8260  fpwwelem  8262  canthwelem  8267  canthwe  8268  pwfseqlem4  8279  wuncss  8362  genpv  8618  genpdm  8621  hashf1lem1  11387  wrdexg  11419  wrdexb  11443  shftfval  11559  o1of2  12080  o1rlimmul  12086  isercolllem2  12133  hashbcss  13045  isstruct2  13151  strssd  13176  ressabs  13200  restid2  13329  prdsbas  13351  divsfval  13443  fnmrc  13503  mrcfval  13504  isacs1i  13553  mreacs  13554  isssc  13691  rescabs  13704  rescabs2  13705  resssetc  13918  resscatc  13931  yonedalem1  14040  yonedalem21  14041  yonedalem3a  14042  yonedalem4c  14045  yonedalem22  14046  yonedalem3b  14047  yonedainv  14049  yonffthlem  14050  ipolerval  14253  gass  14749  symgbas  14766  sylow2a  14924  sylow2blem2  14926  dprdres  15257  islbs3  15902  mplsubglem  16173  mpllsslem  16174  opsrtoslem2  16220  istps3OLD  16654  basdif0  16685  tgval  16687  eltg  16689  eltg2  16690  tgss  16700  basgen2  16721  2basgen  16722  tgdif0  16724  bastop1  16725  lpval  16865  resttopon  16886  restabs  16890  restcld  16897  restfpw  16904  restcls  16905  restntr  16906  ordtbaslem  16912  ordtbas2  16915  ordtbas  16916  ordtrest2  16928  lmfval  16956  cnrest  17007  cnrest2  17008  cnpresti  17010  cnprest  17011  cnprest2  17012  cmpcov  17110  cmpsublem  17120  cmpsub  17121  consuba  17140  consubclo  17144  uncon  17149  2ndcomap  17178  1stcelcls  17181  hausmapdom  17220  ptbasfi  17270  txss12  17294  ptcls  17304  ptrescn  17327  cnmpt2res  17365  qtopval2  17381  elqtop  17382  qtoprest  17402  ptuncnv  17492  ptunhmeo  17493  trfbas2  17532  trfbas  17533  isfildlem  17546  snfbas  17555  fsubbas  17556  trfil1  17575  trfil2  17576  trufil  17599  ssufl  17607  elfm  17636  rnelfmlem  17641  rnelfm  17642  fmfnfmlem4  17646  flimclslem  17673  hauspwpwf1  17676  hauspwpwdom  17677  ptcmplem1  17740  xmetres2  17919  metrest  18064  cnheibor  18447  fmcfil  18692  metcld2  18726  bcthlem1  18740  mbfimaopn2  19006  0pledm  19022  dvbss  19245  dvreslem  19253  dvres2lem  19254  dvcnp2  19263  dvnf  19270  dvnbss  19271  dvaddbr  19281  dvmulbr  19282  dvaddf  19285  dvmulf  19286  dvcmulf  19288  dvcof  19291  dvcnvrelem2  19359  elply2  19572  plyf  19574  plyss  19575  elplyr  19577  plyeq0lem  19586  plyeq0  19587  plyaddlem  19591  plymullem  19592  dgrlem  19605  coeidlem  19613  ulmss  19768  ulmcn  19770  pserulm  19792  issubgo  20962  erdsze2lem1  23138  erdsze2lem2  23139  cvxpcon  23177  cvmliftmolem1  23216  iseupa  23285  dfon2lem3  23542  setlikess  23596  altxpexg  23919  oprabex2gpop  24434  sndw  24498  prjmapcp  24564  prjmapcp2  24569  ubpar  24660  qusp  24941  efilcp  24951  cnfilca  24955  islimrs3  24980  islimrs4  24981  fnctartar3  25308  prismorcsetlem  25311  prismorcset  25313  lemindclsbu  25394  indcls2  25395  ivthALT  25657  islocfin  25695  neibastop2lem  25708  fnejoin1  25716  filnetlem3  25728  filnetlem4  25729  abrexdom  25804  sdclem2  25851  sdclem1  25852  ralxpmap  26160  elrfi  26168  elrfirn  26169  elrfirn2  26170  elmapssres  26191  pwssplit0  26586  pwssplit1  26587  pwssplit2  26588  pwssplit3  26589  pwssplit4  26590  frlmsplit2  26642  frlmsslss  26643  hbtlem1  26726  hbtlem7  26728  pmtrfconj  26806  rabexgf  27094  stoweidlem31  27179  stoweidlem53  27201  stoweidlem57  27205  stoweidlem59  27207  bnj1413  28332
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator