Theorem ssexg 5267

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 3959	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 341	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3443	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5265	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3510	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3439   ⊆ wss 3900

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5240

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-in 3907  df-ss 3917

This theorem is referenced by:  ssexd  5268  prcssprc  5271  difexg  5273  elpw2g  5277  rabexgOLD  5282  elssabg  5287  abssexg  5326  snexALT  5327  sess1  5588  sess2  5589  riinint  5920  resexg  5985  trsuc  6405  ordsssuc2  6409  mptexg  7167  mptexgf  7168  isofr2  7290  ofres  7641  brrpssg  7670  unexb  7692  unexbOLD  7693  xpexg  7695  abnexg  7701  difex2  7705  uniexr  7708  dmexg  7843  rnexg  7844  resiexg  7854  imaexg  7855  exse2  7859  cnvexg  7866  coexg  7871  fabexgOLD  7881  f1oabexgOLD  7885  resfunexgALT  7892  cofunexg  7893  fnexALT  7895  f1dmex  7901  oprabexd  7919  mpoexxg  8019  suppfnss  8131  tposexg  8182  tz7.48-3  8375  oaabs  8576  erex  8660  mapexOLD  8771  pmvalg  8776  elpmg  8782  elmapssres  8806  pmss12g  8809  ralxpmap  8836  ixpexg  8862  domssl  8937  ssdomg  8939  fiprc  8983  domunsncan  9007  infensuc  9085  pssnn  9095  ssfi  9099  enp1i  9181  unbnn  9198  fodomfi  9214  fodomfiOLD  9232  fival  9317  fiss  9329  dffi3  9336  hartogslem2  9450  card2on  9461  wdomima2g  9493  unxpwdom2  9495  unxpwdom  9496  harwdom  9498  oemapvali  9595  ackbij1lem11  10141  cofsmo  10181  ssfin4  10222  fin23lem11  10229  ssfin2  10232  ssfin3ds  10242  isfin1-3  10298  hsmex3  10346  axdc2lem  10360  ac6num  10391  ttukeylem1  10421  dmct  10436  fpwwe2lem3  10546  fpwwe2lem11  10554  fpwwe2lem12  10555  canthwe  10564  wuncss  10658  genpv  10912  genpdm  10915  hashss  14334  wrdexb  14450  shftfval  14995  o1of2  15538  o1rlimmul  15544  isercolllem2  15591  isstruct2  17078  ressval3d  17175  ressabs  17177  prdsbas  17379  fnmrc  17532  mrcfval  17533  isacs1i  17582  mreacs  17583  isssc  17746  ipolerval  18457  chnexg  18543  ress0g  18689  sylow2a  19550  islbs3  21112  toponsspwpw  22868  basdif0  22899  tgval  22901  eltg  22903  eltg2  22904  tgss  22914  basgen2  22935  2basgen  22936  bastop1  22939  topnex  22942  resttopon  23107  restabs  23111  restcld  23118  restfpw  23125  restcls  23127  restntr  23128  ordtbas2  23137  ordtbas  23138  lmfval  23178  cnrest  23231  cmpcov  23335  cmpsublem  23345  cmpsub  23346  2ndcomap  23404  islocfin  23463  txss12  23551  ptrescn  23585  trfbas2  23789  trfbas  23790  isfildlem  23803  snfbas  23812  trfil1  23832  trfil2  23833  trufil  23856  ssufl  23864  hauspwpwf1  23933  ustval  24149  metrest  24470  cnheibor  24912  metcld2  25265  bcthlem1  25282  mbfimaopn2  25616  0pledm  25632  dvbss  25860  dvreslem  25868  dvres2lem  25869  dvcnp2  25879  dvcnp2OLD  25880  dvaddbr  25898  dvmulbr  25899  dvmulbrOLD  25900  dvcnvrelem2  25981  elply2  26159  plyf  26161  plyss  26162  elplyr  26164  plyeq0lem  26173  plyeq0  26174  plyaddlem  26178  plymullem  26179  dgrlem  26192  coeidlem  26200  ulmcn  26366  pserulm  26389  rabexgfGS  32554  abrexdomjm  32562  aciunf1  32721  indval  32911  ress1r  33294  pcmplfin  33996  metidval  34026  sigagenss  34285  measval  34334  omsfval  34430  omssubaddlem  34435  omssubadd  34436  carsggect  34454  fineqvnttrclse  35259  erdsze2lem1  35376  erdsze2lem2  35377  cvxpconn  35415  elmsta  35721  dfon2lem3  35956  altxpexg  36151  ivthALT  36508  filnetlem3  36553  bj-sselpwuni  37224  bj-elpwg  37226  bj-restsnss  37257  bj-restsnss2  37258  bj-restb  37268  bj-restuni2  37272  abrexdom  37900  sdclem2  37912  sdclem1  37913  brssr  38751  sticksstones4  42438  sticksstones14  42449  pssexg  42520  elrfirn  42974  pwssplit4  43368  hbtlem1  43402  hbtlem7  43404  inaex  44575  rabexgf  45306  dvnprodlem2  46228  qndenserrnbllem  46575  sge0ss  46693  psmeasurelem  46751  caragensplit  46781  omeunile  46786  caragenuncl  46794  omeunle  46797  omeiunlempt  46801  carageniuncllem2  46803  fcdmvafv2v  47519  prprval  47797  mpoexxg2  48621  gsumlsscl  48663  lincellss  48709  incat  49883