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

Theorem ssexg 5191
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 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)

Proof of Theorem ssexg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 sseq2 3941 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
21imbi1d 345 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ V) ↔ (𝐴𝐵𝐴 ∈ V)))
3 vex 3444 . . . 4 𝑥 ∈ V
43ssex 5189 . . 3 (𝐴𝑥𝐴 ∈ V)
52, 4vtoclg 3515 . 2 (𝐵𝐶 → (𝐴𝐵𝐴 ∈ V))
65impcom 411 1 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2111  Vcvv 3441  wss 3881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898
This theorem is referenced by:  ssexd  5192  prcssprc  5193  difexg  5195  rabexg  5198  elssabg  5203  elpw2g  5211  abssexg  5248  snexALT  5249  sess1  5487  sess2  5488  riinint  5804  resexg  5864  trsuc  6243  ordsssuc2  6247  mptexg  6961  mptexgf  6962  isofr2  7076  ofres  7405  brrpssg  7431  unexb  7451  xpexg  7453  abnexg  7458  difex2  7462  uniexr  7465  dmexg  7594  rnexg  7595  resiexg  7601  imaexg  7602  exse2  7604  cnvexg  7611  coexg  7616  fabexg  7621  f1oabexg  7624  resfunexgALT  7631  cofunexg  7632  fnexALT  7634  f1dmex  7640  oprabexd  7658  mpoexxg  7756  suppfnss  7838  tposexg  7889  tz7.48-3  8063  oaabs  8254  erex  8296  mapex  8395  pmvalg  8400  elpmg  8405  elmapssres  8414  pmss12g  8416  ralxpmap  8443  ixpexg  8469  ssdomg  8538  fiprc  8578  domunsncan  8600  infensuc  8679  pssnn  8720  unbnn  8758  fodomfi  8781  fival  8860  fiss  8872  dffi3  8879  hartogslem2  8991  card2on  9002  wdomima2g  9034  unxpwdom2  9036  unxpwdom  9037  harwdom  9039  oemapvali  9131  ackbij1lem11  9641  cofsmo  9680  ssfin4  9721  fin23lem11  9728  ssfin2  9731  ssfin3ds  9741  isfin1-3  9797  hsmex3  9845  axdc2lem  9859  ac6num  9890  ttukeylem1  9920  dmct  9935  ondomon  9974  fpwwe2lem3  10044  fpwwe2lem12  10052  fpwwe2lem13  10053  canthwe  10062  wuncss  10156  genpv  10410  genpdm  10413  hashss  13766  hashf1lem1  13809  wrdexb  13868  shftfval  14421  o1of2  14961  o1rlimmul  14967  isercolllem2  15014  isstruct2  16485  ressval3d  16553  ressabs  16555  prdsbas  16722  fnmrc  16870  mrcfval  16871  isacs1i  16920  mreacs  16921  isssc  17082  ipolerval  17758  ress0g  17931  sylow2a  18736  islbs3  19920  toponsspwpw  21527  basdif0  21558  tgval  21560  eltg  21562  eltg2  21563  tgss  21573  basgen2  21594  2basgen  21595  bastop1  21598  topnex  21601  resttopon  21766  restabs  21770  restcld  21777  restfpw  21784  restcls  21786  restntr  21787  ordtbas2  21796  ordtbas  21797  lmfval  21837  cnrest  21890  cmpcov  21994  cmpsublem  22004  cmpsub  22005  2ndcomap  22063  islocfin  22122  txss12  22210  ptrescn  22244  trfbas2  22448  trfbas  22449  isfildlem  22462  snfbas  22471  trfil1  22491  trfil2  22492  trufil  22515  ssufl  22523  hauspwpwf1  22592  ustval  22808  metrest  23131  cnheibor  23560  metcld2  23911  bcthlem1  23928  mbfimaopn2  24261  0pledm  24277  dvbss  24504  dvreslem  24512  dvres2lem  24513  dvcnp2  24523  dvaddbr  24541  dvmulbr  24542  dvcnvrelem2  24621  elply2  24793  plyf  24795  plyss  24796  elplyr  24798  plyeq0lem  24807  plyeq0  24808  plyaddlem  24812  plymullem  24813  dgrlem  24826  coeidlem  24834  ulmcn  24994  pserulm  25017  rabexgfGS  30269  abrexdomjm  30275  aciunf1  30426  ress1r  30911  pcmplfin  31213  metidval  31243  indval  31382  sigagenss  31518  measval  31567  omsfval  31662  omssubaddlem  31667  omssubadd  31668  carsggect  31686  erdsze2lem1  32560  erdsze2lem2  32561  cvxpconn  32599  elmsta  32905  dfon2lem3  33140  altxpexg  33549  ivthALT  33793  filnetlem3  33838  bj-sselpwuni  34464  bj-elpwg  34466  bj-restsnss  34495  bj-restsnss2  34496  bj-restb  34506  bj-restuni2  34510  abrexdom  35165  sdclem2  35177  sdclem1  35178  imaexALTV  35744  brssr  35898  pssexg  39401  elrfirn  39631  pwssplit4  40028  hbtlem1  40062  hbtlem7  40064  inaex  41000  rabexgf  41648  dvnprodlem1  42583  dvnprodlem2  42584  qndenserrnbllem  42931  sge0ss  43046  psmeasurelem  43104  caragensplit  43134  omeunile  43139  caragenuncl  43147  omeunle  43150  omeiunlempt  43154  carageniuncllem2  43156  frnvafv2v  43787  prprval  44026  mpoexxg2  44734  gsumlsscl  44780  lincellss  44830
  Copyright terms: Public domain W3C validator