Theorem ssexg 5303

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Vcvv 3463   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-in 3938  df-ss 3948

This theorem is referenced by:  ssexd  5304  prcssprc  5307  difexg  5309  elpw2g  5313  rabexgOLD  5318  elssabg  5323  abssexg  5362  snexALT  5363  sess1  5630  sess2  5631  riinint  5962  resexg  6025  trsuc  6451  ordsssuc2  6455  mptexg  7223  mptexgf  7224  isofr2  7346  ofres  7698  brrpssg  7727  unexb  7749  unexbOLD  7750  xpexg  7752  abnexg  7758  difex2  7762  uniexr  7765  dmexg  7905  rnexg  7906  resiexg  7916  imaexg  7917  exse2  7921  cnvexg  7928  coexg  7933  fabexgOLD  7943  f1oabexgOLD  7947  resfunexgALT  7954  cofunexg  7955  fnexALT  7957  f1dmex  7963  oprabexd  7982  mpoexxg  8082  suppfnss  8196  tposexg  8247  tz7.48-3  8466  oaabs  8668  erex  8751  mapexOLD  8854  pmvalg  8859  elpmg  8865  elmapssres  8889  pmss12g  8891  ralxpmap  8918  ixpexg  8944  domssl  9020  ssdomg  9022  fiprc  9067  domunsncan  9094  infensuc  9177  pssnn  9190  ssfi  9195  enp1i  9295  unbnn  9314  fodomfi  9332  fodomfiOLD  9352  fival  9434  fiss  9446  dffi3  9453  hartogslem2  9565  card2on  9576  wdomima2g  9608  unxpwdom2  9610  unxpwdom  9611  harwdom  9613  oemapvali  9706  ackbij1lem11  10251  cofsmo  10291  ssfin4  10332  fin23lem11  10339  ssfin2  10342  ssfin3ds  10352  isfin1-3  10408  hsmex3  10456  axdc2lem  10470  ac6num  10501  ttukeylem1  10531  dmct  10546  ondomon  10585  fpwwe2lem3  10655  fpwwe2lem11  10663  fpwwe2lem12  10664  canthwe  10673  wuncss  10767  genpv  11021  genpdm  11024  hashss  14431  wrdexb  14546  shftfval  15092  o1of2  15632  o1rlimmul  15638  isercolllem2  15685  isstruct2  17169  ressval3d  17270  ressabs  17272  prdsbas  17474  fnmrc  17622  mrcfval  17623  isacs1i  17672  mreacs  17673  isssc  17836  ipolerval  18547  ress0g  18745  sylow2a  19606  islbs3  21126  toponsspwpw  22877  basdif0  22908  tgval  22910  eltg  22912  eltg2  22913  tgss  22923  basgen2  22944  2basgen  22945  bastop1  22948  topnex  22951  resttopon  23116  restabs  23120  restcld  23127  restfpw  23134  restcls  23136  restntr  23137  ordtbas2  23146  ordtbas  23147  lmfval  23187  cnrest  23240  cmpcov  23344  cmpsublem  23354  cmpsub  23355  2ndcomap  23413  islocfin  23472  txss12  23560  ptrescn  23594  trfbas2  23798  trfbas  23799  isfildlem  23812  snfbas  23821  trfil1  23841  trfil2  23842  trufil  23865  ssufl  23873  hauspwpwf1  23942  ustval  24158  metrest  24482  cnheibor  24924  metcld2  25278  bcthlem1  25295  mbfimaopn2  25629  0pledm  25645  dvbss  25873  dvreslem  25881  dvres2lem  25882  dvcnp2  25892  dvcnp2OLD  25893  dvaddbr  25911  dvmulbr  25912  dvmulbrOLD  25913  dvcnvrelem2  25994  elply2  26172  plyf  26174  plyss  26175  elplyr  26177  plyeq0lem  26186  plyeq0  26187  plyaddlem  26191  plymullem  26192  dgrlem  26205  coeidlem  26213  ulmcn  26379  pserulm  26402  rabexgfGS  32447  abrexdomjm  32455  aciunf1  32609  indval  32783  ress1r  33182  pcmplfin  33834  metidval  33864  sigagenss  34125  measval  34174  omsfval  34271  omssubaddlem  34276  omssubadd  34277  carsggect  34295  erdsze2lem1  35183  erdsze2lem2  35184  cvxpconn  35222  elmsta  35528  dfon2lem3  35761  altxpexg  35954  ivthALT  36311  filnetlem3  36356  bj-sselpwuni  37026  bj-elpwg  37028  bj-restsnss  37059  bj-restsnss2  37060  bj-restb  37070  bj-restuni2  37074  abrexdom  37712  sdclem2  37724  sdclem1  37725  imaexALTV  38306  brssr  38477  sticksstones4  42125  sticksstones14  42136  pssexg  42240  elrfirn  42684  pwssplit4  43079  hbtlem1  43113  hbtlem7  43115  inaex  44288  rabexgf  45001  dvnprodlem2  45934  qndenserrnbllem  46281  sge0ss  46399  psmeasurelem  46457  caragensplit  46487  omeunile  46492  caragenuncl  46500  omeunle  46503  omeiunlempt  46507  carageniuncllem2  46509  fcdmvafv2v  47221  prprval  47474  mpoexxg2  48227  gsumlsscl  48269  lincellss  48316