Theorem ssexg 5341

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  ssexd  5342  prcssprc  5345  difexg  5347  elpw2g  5351  rabexgOLD  5356  elssabg  5361  abssexg  5400  snexALT  5401  sess1  5665  sess2  5666  riinint  5994  resexg  6056  trsuc  6482  ordsssuc2  6486  mptexg  7258  mptexgf  7259  isofr2  7380  ofres  7733  brrpssg  7760  unexb  7782  unexbOLD  7783  xpexg  7785  abnexg  7791  difex2  7795  uniexr  7798  dmexg  7941  rnexg  7942  resiexg  7952  imaexg  7953  exse2  7957  cnvexg  7964  coexg  7969  fabexgOLD  7977  f1oabexgOLD  7981  resfunexgALT  7988  cofunexg  7989  fnexALT  7991  f1dmex  7997  oprabexd  8016  mpoexxg  8116  suppfnss  8230  tposexg  8281  tz7.48-3  8500  oaabs  8704  erex  8787  mapexOLD  8890  pmvalg  8895  elpmg  8901  elmapssres  8925  pmss12g  8927  ralxpmap  8954  ixpexg  8980  domssl  9058  ssdomg  9060  fiprc  9111  domunsncan  9138  infensuc  9221  pssnn  9234  ssfi  9240  enp1i  9341  unbnn  9360  fodomfi  9378  fodomfiOLD  9398  fival  9481  fiss  9493  dffi3  9500  hartogslem2  9612  card2on  9623  wdomima2g  9655  unxpwdom2  9657  unxpwdom  9658  harwdom  9660  oemapvali  9753  ackbij1lem11  10298  cofsmo  10338  ssfin4  10379  fin23lem11  10386  ssfin2  10389  ssfin3ds  10399  isfin1-3  10455  hsmex3  10503  axdc2lem  10517  ac6num  10548  ttukeylem1  10578  dmct  10593  ondomon  10632  fpwwe2lem3  10702  fpwwe2lem11  10710  fpwwe2lem12  10711  canthwe  10720  wuncss  10814  genpv  11068  genpdm  11071  hashss  14458  wrdexb  14573  shftfval  15119  o1of2  15659  o1rlimmul  15665  isercolllem2  15714  isstruct2  17196  ressval3d  17305  ressval3dOLD  17306  ressabs  17308  prdsbas  17517  fnmrc  17665  mrcfval  17666  isacs1i  17715  mreacs  17716  isssc  17881  ipolerval  18602  ress0g  18800  sylow2a  19661  islbs3  21180  toponsspwpw  22949  basdif0  22981  tgval  22983  eltg  22985  eltg2  22986  tgss  22996  basgen2  23017  2basgen  23018  bastop1  23021  topnex  23024  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  24558  cnheibor  25006  metcld2  25360  bcthlem1  25377  mbfimaopn2  25711  0pledm  25727  dvbss  25956  dvreslem  25964  dvres2lem  25965  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcnvrelem2  26077  elply2  26255  plyf  26257  plyss  26258  elplyr  26260  plyeq0lem  26269  plyeq0  26270  plyaddlem  26274  plymullem  26275  dgrlem  26288  coeidlem  26296  ulmcn  26460  pserulm  26483  rabexgfGS  32527  abrexdomjm  32535  aciunf1  32681  ress1r  33214  pcmplfin  33806  metidval  33836  indval  33977  sigagenss  34113  measval  34162  omsfval  34259  omssubaddlem  34264  omssubadd  34265  carsggect  34283  erdsze2lem1  35171  erdsze2lem2  35172  cvxpconn  35210  elmsta  35516  dfon2lem3  35749  altxpexg  35942  ivthALT  36301  filnetlem3  36346  bj-sselpwuni  37016  bj-elpwg  37018  bj-restsnss  37049  bj-restsnss2  37050  bj-restb  37060  bj-restuni2  37064  abrexdom  37690  sdclem2  37702  sdclem1  37703  imaexALTV  38286  brssr  38457  sticksstones4  42106  sticksstones14  42117  pssexg  42219  elrfirn  42651  pwssplit4  43046  hbtlem1  43080  hbtlem7  43082  inaex  44266  rabexgf  44924  dvnprodlem1  45867  dvnprodlem2  45868  qndenserrnbllem  46215  sge0ss  46333  psmeasurelem  46391  caragensplit  46421  omeunile  46426  caragenuncl  46434  omeunle  46437  omeiunlempt  46441  carageniuncllem2  46443  fcdmvafv2v  47151  prprval  47388  mpoexxg2  48062  gsumlsscl  48108  lincellss  48155