Theorem ssexg 5269

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.

Step	Hyp	Ref	Expression
1		sseq2 3953	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 343	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3448	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5267	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3512	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 410	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1550   ∈ wcel 2132  Vcvv 3444   ⊆ wss 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1097  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-in 3902  df-ss 3912

This theorem is referenced by:  ssexd  5270  prcssprc  5273  difexg  5275  elpw2g  5279  rabexgOLD  5284  elssabg  5289  abssexg  5329  snexALT  5330  sess1  5601  sess2  5602  riinint  5937  resexg  6002  trsuc  6420  ordsssuc2  6424  mptexg  7190  mptexgf  7191  isofr2  7313  ofres  7664  brrpssg  7693  unexb  7715  unexbOLD  7716  xpexg  7718  abnexg  7724  difex2  7728  uniexr  7731  dmexg  7867  rnexg  7868  resiexg  7878  imaexg  7879  exse2  7883  cnvexg  7890  coexg  7895  resfunexgALT  7914  cofunexg  7915  fnexALT  7917  f1dmex  7923  oprabexd  7941  mpoexxg  8041  suppfnss  8153  tposexg  8204  tz7.48-3  8399  oaabs  8602  erex  8687  mapexOLD  8798  pmvalg  8803  elpmg  8809  elmapssres  8833  pmss12g  8836  ralxpmap  8863  ixpexg  8889  domssl  8964  ssdomg  8966  fiprc  9010  domunsncan  9034  infensuc  9112  pssnn  9122  ssfi  9126  enp1i  9208  unbnn  9225  fodomfi  9241  fodomfiOLD  9259  fival  9344  fiss  9356  dffi3  9363  hartogslem2  9477  card2on  9488  wdomima2g  9520  unxpwdom2  9522  unxpwdom  9523  harwdom  9525  oemapvali  9625  ackbij1lem11  10171  cofsmo  10212  ssfin4  10253  fin23lem11  10260  ssfin2  10263  ssfin3ds  10273  isfin1-3  10329  hsmex3  10377  axdc2lem  10391  ac6num  10422  ttukeylem1  10452  dmct  10467  fpwwe2lem3  10577  fpwwe2lem11  10585  fpwwe2lem12  10586  canthwe  10595  wuncss  10689  genpv  10943  genpdm  10946  indval  12184  hashss  14408  wrdexb  14524  shftfval  15069  o1of2  15612  o1rlimmul  15618  isercolllem2  15665  isstruct2  17157  ressval3d  17254  ressabs  17256  prdsbas  17458  fnmrc  17611  mrcfval  17612  isacs1i  17661  mreacs  17662  isssc  17825  ipolerval  18536  chnexg  18622  ress0g  18768  sylow2a  19631  islbs3  21194  toponsspwpw  22951  basdif0  22982  tgval  22984  eltg  22986  eltg2  22987  tgss  22997  basgen2  23018  2basgen  23019  bastop1  23022  topnex  23025  resttopon  23190  restabs  23194  restcld  23201  restfpw  23208  restcls  23210  restntr  23211  ordtbas2  23220  ordtbas  23221  lmfval  23261  cnrest  23314  cmpcov  23418  cmpsublem  23428  cmpsub  23429  2ndcomap  23487  islocfin  23546  txss12  23634  ptrescn  23668  trfbas2  23872  trfbas  23873  isfildlem  23886  snfbas  23895  trfil1  23915  trfil2  23916  trufil  23939  ssufl  23947  hauspwpwf1  24016  ustval  24232  metrest  24553  cnheibor  24986  metcld2  25338  bcthlem1  25355  mbfimaopn2  25688  0pledm  25704  dvbss  25932  dvreslem  25940  dvres2lem  25941  dvcnp2  25951  dvaddbr  25969  dvmulbr  25970  dvcnvrelem2  26049  elply2  26225  plyf  26227  plyss  26228  elplyr  26230  plyeq0lem  26239  plyeq0  26240  plyaddlem  26244  plymullem  26245  dgrlem  26258  coeidlem  26266  ulmcn  26428  pserulm  26451  rabexgfGS  32636  abrexdomjm  32644  aciunf1  32804  ress1r  33363  pcmplfin  34101  metidval  34131  sigagenss  34390  measval  34439  omsfval  34535  omssubaddlem  34540  omssubadd  34541  carsggect  34559  fineqvnttrclse  35365  erdsze2lem1  35491  erdsze2lem2  35492  cvxpconn  35530  elmsta  35836  dfon2lem3  36071  altxpexg  36266  ivthALT  36633  filnetlem3  36678  ttcexrg  36795  ttcsnexbig  36819  ttcexg  36830  bj-sselpwuni  37473  bj-elpwg  37475  bj-restsnss  37511  bj-restsnss2  37512  bj-restb  37522  bj-restuni2  37526  abrexdom  38167  sdclem2  38179  sdclem1  38180  brssr  39018  sticksstones4  42704  sticksstones14  42715  pssexg  42783  elrfirn  43214  pwssplit4  43604  hbtlem1  43638  hbtlem7  43640  inaex  44811  rabexgf  45542  dvnprodlem2  46459  qndenserrnbllem  46806  sge0ss  46924  psmeasurelem  46982  caragensplit  47012  omeunile  47017  caragenuncl  47025  omeunle  47028  omeiunlempt  47032  carageniuncllem2  47034  fcdmvafv2v  47768  prprval  48058  mpoexxg2  48898  gsumlsscl  48940  lincellss  48986  incat  50160