Theorem ssexg 5262

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

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

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920

This theorem is referenced by:  ssexd  5263  prcssprc  5266  difexg  5268  elpw2g  5272  rabexgOLD  5277  elssabg  5282  abssexg  5321  snexALT  5322  sess1  5584  sess2  5585  riinint  5913  resexg  5978  trsuc  6396  ordsssuc2  6400  mptexg  7157  mptexgf  7158  isofr2  7281  ofres  7632  brrpssg  7661  unexb  7683  unexbOLD  7684  xpexg  7686  abnexg  7692  difex2  7696  uniexr  7699  dmexg  7834  rnexg  7835  resiexg  7845  imaexg  7846  exse2  7850  cnvexg  7857  coexg  7862  fabexgOLD  7872  f1oabexgOLD  7876  resfunexgALT  7883  cofunexg  7884  fnexALT  7886  f1dmex  7892  oprabexd  7910  mpoexxg  8010  suppfnss  8122  tposexg  8173  tz7.48-3  8366  oaabs  8566  erex  8649  mapexOLD  8759  pmvalg  8764  elpmg  8770  elmapssres  8794  pmss12g  8796  ralxpmap  8823  ixpexg  8849  domssl  8923  ssdomg  8925  fiprc  8970  domunsncan  8994  infensuc  9072  pssnn  9082  ssfi  9087  enp1i  9168  unbnn  9185  fodomfi  9201  fodomfiOLD  9220  fival  9302  fiss  9314  dffi3  9321  hartogslem2  9435  card2on  9446  wdomima2g  9478  unxpwdom2  9480  unxpwdom  9481  harwdom  9483  oemapvali  9580  ackbij1lem11  10123  cofsmo  10163  ssfin4  10204  fin23lem11  10211  ssfin2  10214  ssfin3ds  10224  isfin1-3  10280  hsmex3  10328  axdc2lem  10342  ac6num  10373  ttukeylem1  10403  dmct  10418  ondomon  10457  fpwwe2lem3  10527  fpwwe2lem11  10535  fpwwe2lem12  10536  canthwe  10545  wuncss  10639  genpv  10893  genpdm  10896  hashss  14316  wrdexb  14432  shftfval  14977  o1of2  15520  o1rlimmul  15526  isercolllem2  15573  isstruct2  17060  ressval3d  17157  ressabs  17159  prdsbas  17361  fnmrc  17513  mrcfval  17514  isacs1i  17563  mreacs  17564  isssc  17727  ipolerval  18438  ress0g  18636  sylow2a  19498  islbs3  21062  toponsspwpw  22807  basdif0  22838  tgval  22840  eltg  22842  eltg2  22843  tgss  22853  basgen2  22874  2basgen  22875  bastop1  22878  topnex  22881  resttopon  23046  restabs  23050  restcld  23057  restfpw  23064  restcls  23066  restntr  23067  ordtbas2  23076  ordtbas  23077  lmfval  23117  cnrest  23170  cmpcov  23274  cmpsublem  23284  cmpsub  23285  2ndcomap  23343  islocfin  23402  txss12  23490  ptrescn  23524  trfbas2  23728  trfbas  23729  isfildlem  23742  snfbas  23751  trfil1  23771  trfil2  23772  trufil  23795  ssufl  23803  hauspwpwf1  23872  ustval  24088  metrest  24410  cnheibor  24852  metcld2  25205  bcthlem1  25222  mbfimaopn2  25556  0pledm  25572  dvbss  25800  dvreslem  25808  dvres2lem  25809  dvcnp2  25819  dvcnp2OLD  25820  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcnvrelem2  25921  elply2  26099  plyf  26101  plyss  26102  elplyr  26104  plyeq0lem  26113  plyeq0  26114  plyaddlem  26118  plymullem  26119  dgrlem  26132  coeidlem  26140  ulmcn  26306  pserulm  26329  rabexgfGS  32448  abrexdomjm  32456  aciunf1  32614  indval  32805  ress1r  33183  pcmplfin  33843  metidval  33873  sigagenss  34132  measval  34181  omsfval  34278  omssubaddlem  34283  omssubadd  34284  carsggect  34302  fineqvnttrclse  35093  erdsze2lem1  35196  erdsze2lem2  35197  cvxpconn  35235  elmsta  35541  dfon2lem3  35779  altxpexg  35972  ivthALT  36329  filnetlem3  36374  bj-sselpwuni  37044  bj-elpwg  37046  bj-restsnss  37077  bj-restsnss2  37078  bj-restb  37088  bj-restuni2  37092  abrexdom  37730  sdclem2  37742  sdclem1  37743  brssr  38498  sticksstones4  42142  sticksstones14  42153  pssexg  42219  elrfirn  42688  pwssplit4  43082  hbtlem1  43116  hbtlem7  43118  inaex  44290  rabexgf  45022  dvnprodlem2  45948  qndenserrnbllem  46295  sge0ss  46413  psmeasurelem  46471  caragensplit  46501  omeunile  46506  caragenuncl  46514  omeunle  46517  omeiunlempt  46521  carageniuncllem2  46523  fcdmvafv2v  47240  prprval  47518  mpoexxg2  48342  gsumlsscl  48384  lincellss  48431  incat  49606