Theorem ssexg 5263

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

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

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 2709  ax-sep 5232

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  ssexd  5264  prcssprc  5267  difexg  5269  elpw2g  5273  rabexgOLD  5278  elssabg  5283  abssexg  5323  snexALT  5324  sess1  5593  sess2  5594  riinint  5925  resexg  5990  trsuc  6410  ordsssuc2  6414  mptexg  7173  mptexgf  7174  isofr2  7296  ofres  7647  brrpssg  7676  unexb  7698  unexbOLD  7699  xpexg  7701  abnexg  7707  difex2  7711  uniexr  7714  dmexg  7849  rnexg  7850  resiexg  7860  imaexg  7861  exse2  7865  cnvexg  7872  coexg  7877  fabexgOLD  7887  f1oabexgOLD  7891  resfunexgALT  7898  cofunexg  7899  fnexALT  7901  f1dmex  7907  oprabexd  7925  mpoexxg  8025  suppfnss  8136  tposexg  8187  tz7.48-3  8380  oaabs  8581  erex  8665  mapexOLD  8776  pmvalg  8781  elpmg  8787  elmapssres  8811  pmss12g  8814  ralxpmap  8841  ixpexg  8867  domssl  8942  ssdomg  8944  fiprc  8988  domunsncan  9012  infensuc  9090  pssnn  9100  ssfi  9104  enp1i  9186  unbnn  9203  fodomfi  9219  fodomfiOLD  9237  fival  9322  fiss  9334  dffi3  9341  hartogslem2  9455  card2on  9466  wdomima2g  9498  unxpwdom2  9500  unxpwdom  9501  harwdom  9503  oemapvali  9602  ackbij1lem11  10148  cofsmo  10188  ssfin4  10229  fin23lem11  10236  ssfin2  10239  ssfin3ds  10249  isfin1-3  10305  hsmex3  10353  axdc2lem  10367  ac6num  10398  ttukeylem1  10428  dmct  10443  fpwwe2lem3  10553  fpwwe2lem11  10561  fpwwe2lem12  10562  canthwe  10571  wuncss  10665  genpv  10919  genpdm  10922  indval  12159  hashss  14368  wrdexb  14484  shftfval  15029  o1of2  15572  o1rlimmul  15578  isercolllem2  15625  isstruct2  17116  ressval3d  17213  ressabs  17215  prdsbas  17417  fnmrc  17570  mrcfval  17571  isacs1i  17620  mreacs  17621  isssc  17784  ipolerval  18495  chnexg  18581  ress0g  18727  sylow2a  19591  islbs3  21151  toponsspwpw  22903  basdif0  22934  tgval  22936  eltg  22938  eltg2  22939  tgss  22949  basgen2  22970  2basgen  22971  bastop1  22974  topnex  22977  resttopon  23142  restabs  23146  restcld  23153  restfpw  23160  restcls  23162  restntr  23163  ordtbas2  23172  ordtbas  23173  lmfval  23213  cnrest  23266  cmpcov  23370  cmpsublem  23380  cmpsub  23381  2ndcomap  23439  islocfin  23498  txss12  23586  ptrescn  23620  trfbas2  23824  trfbas  23825  isfildlem  23838  snfbas  23847  trfil1  23867  trfil2  23868  trufil  23891  ssufl  23899  hauspwpwf1  23968  ustval  24184  metrest  24505  cnheibor  24938  metcld2  25290  bcthlem1  25307  mbfimaopn2  25640  0pledm  25656  dvbss  25884  dvreslem  25892  dvres2lem  25893  dvcnp2  25903  dvaddbr  25921  dvmulbr  25922  dvcnvrelem2  26001  elply2  26177  plyf  26179  plyss  26180  elplyr  26182  plyeq0lem  26191  plyeq0  26192  plyaddlem  26196  plymullem  26197  dgrlem  26210  coeidlem  26218  ulmcn  26383  pserulm  26406  rabexgfGS  32590  abrexdomjm  32598  aciunf1  32757  ress1r  33315  pcmplfin  34026  metidval  34056  sigagenss  34315  measval  34364  omsfval  34460  omssubaddlem  34465  omssubadd  34466  carsggect  34484  fineqvnttrclse  35290  erdsze2lem1  35407  erdsze2lem2  35408  cvxpconn  35446  elmsta  35752  dfon2lem3  35987  altxpexg  36182  ivthALT  36539  filnetlem3  36584  ttcexrg  36701  ttcsnexbig  36725  ttcexg  36736  bj-sselpwuni  37379  bj-elpwg  37381  bj-restsnss  37417  bj-restsnss2  37418  bj-restb  37428  bj-restuni2  37432  abrexdom  38073  sdclem2  38085  sdclem1  38086  brssr  38924  sticksstones4  42610  sticksstones14  42621  pssexg  42689  elrfirn  43149  pwssplit4  43543  hbtlem1  43577  hbtlem7  43579  inaex  44750  rabexgf  45481  dvnprodlem2  46401  qndenserrnbllem  46748  sge0ss  46866  psmeasurelem  46924  caragensplit  46954  omeunile  46959  caragenuncl  46967  omeunle  46970  omeiunlempt  46974  carageniuncllem2  46976  fcdmvafv2v  47704  prprval  47994  mpoexxg2  48834  gsumlsscl  48876  lincellss  48922  incat  50096