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

Theorem ssexg 4120
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 3161 . . . 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 2760 . . . 4  |-  x  e. 
_V
43ssex 4118 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2811 . 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 2757    C_ wss 3113
This theorem is referenced by:  ssexd  4121  difexg  4122  rabexg  4124  elssabg  4126  elpw2g  4127  abssexg  4153  snexALT  4154  sess1  4319  sess2  4320  trsuc  4434  ordsssuc2  4439  unexb  4478  difex2  4483  uniexb  4521  xpexg  4774  riinint  4909  dmexg  4913  rnexg  4914  resexg  4968  resiexg  4971  imaexg  5000  exse2  5021  soex  5096  cnvexg  5181  coexg  5188  fex2  5325  fabexg  5346  f1oabexg  5408  resfunexgALT  5658  cofunexg  5659  fnexALT  5662  mptexg  5665  f1dmex  5671  isofr2  5761  oprabexd  5880  ofres  6014  mpt2exxg  6115  fnwelem  6150  fnse  6152  tposexg  6168  brrpssg  6199  tz7.48-3  6410  oaabs  6596  erex  6638  mapex  6732  pmvalg  6737  elpmg  6740  pmss12g  6748  ixpexg  6794  ssdomg  6861  f1imaen2g  6876  fiprc  6896  domunsncan  6916  infensuc  6993  pssnn  7035  unbnn  7067  fodomfi  7089  fival  7120  fiss  7131  dffi3  7138  ordtypelem10  7196  oismo  7209  hartogslem2  7212  wofib  7214  wemapso  7220  card2on  7222  wdom2d  7248  wdomd  7249  wdomima2g  7254  unxpwdom2  7256  unxpwdom  7257  harwdom  7258  cantnfle  7326  cantnflt  7327  cantnflt2  7328  cantnfp1lem2  7335  cantnfp1lem3  7336  oemapvali  7340  cantnflem1b  7342  cantnflem1d  7344  cantnflem1  7345  cnfcomlem  7356  cnfcom  7357  cnfcom2lem  7358  cnfcom3lem  7360  acni2  7627  ackbij1lem11  7810  cofsmo  7849  ssfin4  7890  fin23lem11  7897  ssfin2  7900  ssfin3ds  7910  isfin1-3  7966  fin1a2lem12  7991  hsmexlem1  8006  hsmex3  8014  axdc2lem  8028  ac6num  8060  zorn2lem1  8077  zorn2lem4  8080  ttukeylem1  8090  ondomon  8139  fpwwe2lem2  8208  fpwwe2lem3  8209  fpwwe2lem5  8210  fpwwe2lem12  8217  fpwwe2lem13  8218  fpwwe2  8219  fpwwelem  8221  canthwelem  8226  canthwe  8227  pwfseqlem4  8238  wuncss  8321  genpv  8577  genpdm  8580  hashf1lem1  11344  wrdexg  11376  wrdexb  11400  shftfval  11516  o1of2  12037  o1rlimmul  12043  isercolllem2  12090  hashbcss  12999  isstruct2  13105  strssd  13130  ressabs  13154  restid2  13283  prdsbas  13305  divsfval  13397  fnmrc  13457  mrcfval  13458  isacs1i  13507  mreacs  13508  isssc  13645  rescabs  13658  rescabs2  13659  resssetc  13872  resscatc  13885  yonedalem1  13994  yonedalem21  13995  yonedalem3a  13996  yonedalem4c  13999  yonedalem22  14000  yonedalem3b  14001  yonedainv  14003  yonffthlem  14004  ipolerval  14207  gass  14703  symgbas  14720  sylow2a  14878  sylow2blem2  14880  dprdres  15211  islbs3  15856  mplsubglem  16127  mpllsslem  16128  opsrtoslem2  16174  istps3OLD  16608  basdif0  16639  tgval  16641  eltg  16643  eltg2  16644  tgss  16654  basgen2  16675  2basgen  16676  tgdif0  16678  bastop1  16679  lpval  16819  resttopon  16840  restabs  16844  restcld  16851  restfpw  16858  restcls  16859  restntr  16860  ordtbaslem  16866  ordtbas2  16869  ordtbas  16870  ordtrest2  16882  lmfval  16910  cnrest  16961  cnrest2  16962  cnpresti  16964  cnprest  16965  cnprest2  16966  cmpcov  17064  cmpsublem  17074  cmpsub  17075  consuba  17094  consubclo  17098  uncon  17103  2ndcomap  17132  1stcelcls  17135  hausmapdom  17174  ptbasfi  17224  txss12  17248  ptcls  17258  ptrescn  17281  cnmpt2res  17319  qtopval2  17335  elqtop  17336  qtoprest  17356  ptuncnv  17446  ptunhmeo  17447  trfbas2  17486  trfbas  17487  isfildlem  17500  snfbas  17509  fsubbas  17510  trfil1  17529  trfil2  17530  trufil  17553  ssufl  17561  elfm  17590  rnelfmlem  17595  rnelfm  17596  fmfnfmlem4  17600  flimclslem  17627  hauspwpwf1  17630  hauspwpwdom  17631  ptcmplem1  17694  xmetres2  17873  metrest  18018  cnheibor  18401  fmcfil  18646  metcld2  18680  bcthlem1  18694  mbfimaopn2  18960  0pledm  18976  dvbss  19199  dvreslem  19207  dvres2lem  19208  dvcnp2  19217  dvnf  19224  dvnbss  19225  dvaddbr  19235  dvmulbr  19236  dvaddf  19239  dvmulf  19240  dvcmulf  19242  dvcof  19245  dvcnvrelem2  19313  elply2  19526  plyf  19528  plyss  19529  elplyr  19531  plyeq0lem  19540  plyeq0  19541  plyaddlem  19545  plymullem  19546  dgrlem  19559  coeidlem  19567  ulmss  19722  ulmcn  19724  pserulm  19746  issubgo  20916  erdsze2lem1  23092  erdsze2lem2  23093  cvxpcon  23131  cvmliftmolem1  23170  iseupa  23239  dfon2lem3  23496  setlikess  23550  altxpexg  23873  oprabex2gpop  24388  sndw  24452  prjmapcp  24518  prjmapcp2  24523  ubpar  24614  qusp  24895  efilcp  24905  cnfilca  24909  islimrs3  24934  islimrs4  24935  fnctartar3  25262  prismorcsetlem  25265  prismorcset  25267  lemindclsbu  25348  indcls2  25349  ivthALT  25611  islocfin  25649  neibastop2lem  25662  fnejoin1  25670  filnetlem3  25682  filnetlem4  25683  abrexdom  25758  sdclem2  25805  sdclem1  25806  ralxpmap  26114  elrfi  26122  elrfirn  26123  elrfirn2  26124  elmapssres  26145  pwssplit0  26540  pwssplit1  26541  pwssplit2  26542  pwssplit3  26543  pwssplit4  26544  frlmsplit2  26596  frlmsslss  26597  hbtlem1  26680  hbtlem7  26682  pmtrfconj  26760  rabexgf  27049  stoweidlem31  27101  stoweidlem53  27123  stoweidlem57  27127  stoweidlem59  27129  bnj1413  28098
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 1927  ax-ext 2237  ax-sep 4101
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator