Theorem ssexg 5273

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  ssexd  5274  prcssprc  5277  difexg  5279  elpw2g  5283  rabexgOLD  5288  elssabg  5293  abssexg  5332  snexALT  5333  sess1  5596  sess2  5597  riinint  5925  resexg  5988  trsuc  6410  ordsssuc2  6414  mptexg  7178  mptexgf  7179  isofr2  7302  ofres  7653  brrpssg  7682  unexb  7704  unexbOLD  7705  xpexg  7707  abnexg  7713  difex2  7717  uniexr  7720  dmexg  7858  rnexg  7859  resiexg  7869  imaexg  7870  exse2  7874  cnvexg  7881  coexg  7886  fabexgOLD  7896  f1oabexgOLD  7900  resfunexgALT  7907  cofunexg  7908  fnexALT  7910  f1dmex  7916  oprabexd  7934  mpoexxg  8034  suppfnss  8146  tposexg  8197  tz7.48-3  8390  oaabs  8590  erex  8673  mapexOLD  8783  pmvalg  8788  elpmg  8794  elmapssres  8818  pmss12g  8820  ralxpmap  8847  ixpexg  8873  domssl  8947  ssdomg  8949  fiprc  8994  domunsncan  9019  infensuc  9097  pssnn  9110  ssfi  9115  enp1i  9201  unbnn  9220  fodomfi  9238  fodomfiOLD  9258  fival  9340  fiss  9352  dffi3  9359  hartogslem2  9473  card2on  9484  wdomima2g  9516  unxpwdom2  9518  unxpwdom  9519  harwdom  9521  oemapvali  9616  ackbij1lem11  10161  cofsmo  10201  ssfin4  10242  fin23lem11  10249  ssfin2  10252  ssfin3ds  10262  isfin1-3  10318  hsmex3  10366  axdc2lem  10380  ac6num  10411  ttukeylem1  10441  dmct  10456  ondomon  10495  fpwwe2lem3  10565  fpwwe2lem11  10573  fpwwe2lem12  10574  canthwe  10583  wuncss  10677  genpv  10931  genpdm  10934  hashss  14353  wrdexb  14469  shftfval  15014  o1of2  15557  o1rlimmul  15563  isercolllem2  15610  isstruct2  17097  ressval3d  17194  ressabs  17196  prdsbas  17398  fnmrc  17550  mrcfval  17551  isacs1i  17600  mreacs  17601  isssc  17764  ipolerval  18475  ress0g  18673  sylow2a  19535  islbs3  21099  toponsspwpw  22844  basdif0  22875  tgval  22877  eltg  22879  eltg2  22880  tgss  22890  basgen2  22911  2basgen  22912  bastop1  22915  topnex  22918  resttopon  23083  restabs  23087  restcld  23094  restfpw  23101  restcls  23103  restntr  23104  ordtbas2  23113  ordtbas  23114  lmfval  23154  cnrest  23207  cmpcov  23311  cmpsublem  23321  cmpsub  23322  2ndcomap  23380  islocfin  23439  txss12  23527  ptrescn  23561  trfbas2  23765  trfbas  23766  isfildlem  23779  snfbas  23788  trfil1  23808  trfil2  23809  trufil  23832  ssufl  23840  hauspwpwf1  23909  ustval  24125  metrest  24447  cnheibor  24889  metcld2  25242  bcthlem1  25259  mbfimaopn2  25593  0pledm  25609  dvbss  25837  dvreslem  25845  dvres2lem  25846  dvcnp2  25856  dvcnp2OLD  25857  dvaddbr  25875  dvmulbr  25876  dvmulbrOLD  25877  dvcnvrelem2  25958  elply2  26136  plyf  26138  plyss  26139  elplyr  26141  plyeq0lem  26150  plyeq0  26151  plyaddlem  26155  plymullem  26156  dgrlem  26169  coeidlem  26177  ulmcn  26343  pserulm  26366  rabexgfGS  32480  abrexdomjm  32488  aciunf1  32639  indval  32828  ress1r  33203  pcmplfin  33845  metidval  33875  sigagenss  34134  measval  34183  omsfval  34280  omssubaddlem  34285  omssubadd  34286  carsggect  34304  erdsze2lem1  35185  erdsze2lem2  35186  cvxpconn  35224  elmsta  35530  dfon2lem3  35768  altxpexg  35961  ivthALT  36318  filnetlem3  36363  bj-sselpwuni  37033  bj-elpwg  37035  bj-restsnss  37066  bj-restsnss2  37067  bj-restb  37077  bj-restuni2  37081  abrexdom  37719  sdclem2  37731  sdclem1  37732  brssr  38487  sticksstones4  42132  sticksstones14  42143  pssexg  42209  elrfirn  42678  pwssplit4  43073  hbtlem1  43107  hbtlem7  43109  inaex  44281  rabexgf  45013  dvnprodlem2  45940  qndenserrnbllem  46287  sge0ss  46405  psmeasurelem  46463  caragensplit  46493  omeunile  46498  caragenuncl  46506  omeunle  46509  omeiunlempt  46513  carageniuncllem2  46515  fcdmvafv2v  47232  prprval  47510  mpoexxg2  48321  gsumlsscl  48363  lincellss  48410  incat  49585