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

Theorem ssexg 4726
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 3589 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
21imbi1d 329 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ V) ↔ (𝐴𝐵𝐴 ∈ V)))
3 vex 3175 . . . 4 𝑥 ∈ V
43ssex 4724 . . 3 (𝐴𝑥𝐴 ∈ V)
52, 4vtoclg 3238 . 2 (𝐵𝐶 → (𝐴𝐵𝐴 ∈ V))
65impcom 444 1 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  Vcvv 3172  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553
This theorem is referenced by:  ssexd  4727  difexg  4729  rabexg  4733  elssabg  4740  elpw2g  4748  abssexg  4771  snexALT  4772  sess1  4995  sess2  4996  riinint  5289  resexg  5348  trsuc  5712  ordsssuc2  5716  mptexg  6366  isofr2  6471  ofres  6788  brrpssg  6814  unexb  6833  xpexg  6835  difex2  6840  uniexb  6843  dmexg  6966  rnexg  6967  resiexg  6971  imaexg  6972  exse2  6975  cnvexg  6982  coexg  6987  fabexg  6992  f1oabexg  6995  resfunexgALT  6999  cofunexg  7000  fnexALT  7002  f1dmex  7006  oprabexd  7023  mpt2exxg  7110  suppfnss  7184  tposexg  7230  tz7.48-3  7403  oaabs  7588  erex  7630  mapex  7727  pmvalg  7732  elpmg  7736  elmapssres  7745  pmss12g  7747  ralxpmap  7770  ixpexg  7795  ssdomg  7864  fiprc  7901  domunsncan  7922  infensuc  8000  pssnn  8040  unbnn  8078  fodomfi  8101  fival  8178  fiss  8190  dffi3  8197  hartogslem2  8308  card2on  8319  wdomima2g  8351  unxpwdom2  8353  unxpwdom  8354  harwdom  8355  oemapvali  8441  ackbij1lem11  8912  cofsmo  8951  ssfin4  8992  fin23lem11  8999  ssfin2  9002  ssfin3ds  9012  isfin1-3  9068  hsmex3  9116  axdc2lem  9130  ac6num  9161  ttukeylem1  9191  ondomon  9241  fpwwe2lem3  9311  fpwwe2lem12  9319  fpwwe2lem13  9320  canthwe  9329  wuncss  9423  genpv  9677  genpdm  9680  hashss  13012  hashf1lem1  13050  wrdexg  13118  wrdexb  13119  shftfval  13606  o1of2  14139  o1rlimmul  14145  isercolllem2  14192  isstruct2  15652  ressval3d  15712  ressabs  15714  prdsbas  15888  fnmrc  16038  mrcfval  16039  isacs1i  16089  mreacs  16090  isssc  16251  ipolerval  16927  ress0g  17090  symgbas  17571  sylow2a  17805  islbs3  18924  basdif0  20515  tgval  20517  eltg  20519  eltg2  20520  tgss  20530  basgen2  20551  2basgen  20552  bastop1  20555  resttopon  20722  restabs  20726  restcld  20733  restfpw  20740  restcls  20742  restntr  20743  ordtbas2  20752  ordtbas  20753  lmfval  20793  cnrest  20846  cmpcov  20949  cmpsublem  20959  cmpsub  20960  2ndcomap  21018  islocfin  21077  txss12  21165  ptrescn  21199  trfbas2  21404  trfbas  21405  isfildlem  21418  snfbas  21427  trfil1  21447  trfil2  21448  trufil  21471  ssufl  21479  hauspwpwf1  21548  ustval  21763  metrest  22086  cnheibor  22509  metcld2  22857  bcthlem1  22873  mbfimaopn2  23174  0pledm  23190  dvbss  23415  dvreslem  23423  dvres2lem  23424  dvcnp2  23433  dvaddbr  23451  dvmulbr  23452  dvcnvrelem2  23529  elply2  23700  plyf  23702  plyss  23703  elplyr  23705  plyeq0lem  23714  plyeq0  23715  plyaddlem  23719  plymullem  23720  dgrlem  23733  coeidlem  23741  ulmcn  23901  pserulm  23924  iseupa  26285  rabexgfGS  28518  abrexdomjm  28522  mptexgf  28602  aciunf1  28638  dmct  28670  ress1r  28913  pcmplfin  29048  metidval  29054  indval  29196  sigagenss  29332  measval  29381  omsfval  29476  omssubaddlem  29481  omssubadd  29482  elcarsg  29487  carsggect  29500  erdsze2lem1  30232  erdsze2lem2  30233  cvxpcon  30271  elmsta  30492  dfon2lem3  30727  altxpexg  31048  ivthALT  31293  filnetlem3  31338  bj-restsnss  32000  bj-restsnss2  32001  bj-restb  32011  bj-restuni2  32015  bj-toponss  32024  bj-topnex  32030  abrexdom  32478  sdclem2  32491  sdclem1  32492  elrfirn  36059  pwssplit4  36460  hbtlem1  36495  hbtlem7  36497  rabexgf  37989  wessf1ornlem  38149  disjinfi  38158  dvnprodlem1  38619  dvnprodlem2  38620  qndenserrnbllem  38973  sge0ss  39088  psmeasurelem  39146  caragensplit  39173  omeunile  39178  caragenuncl  39186  omeunle  39189  omeiunlempt  39193  carageniuncllem2  39195  prcssprc  40090  mpt2exxg2  41890  gsumlsscl  41939  lincellss  41990
  Copyright terms: Public domain W3C validator