Theorem ssexg 5328

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  ssexd  5329  prcssprc  5332  difexg  5334  elpw2g  5338  rabexgOLD  5343  elssabg  5348  abssexg  5387  snexALT  5388  sess1  5653  sess2  5654  riinint  5984  resexg  6046  trsuc  6472  ordsssuc2  6476  mptexg  7240  mptexgf  7241  isofr2  7363  ofres  7715  brrpssg  7743  unexb  7765  unexbOLD  7766  xpexg  7768  abnexg  7774  difex2  7778  uniexr  7781  dmexg  7923  rnexg  7924  resiexg  7934  imaexg  7935  exse2  7939  cnvexg  7946  coexg  7951  fabexgOLD  7959  f1oabexgOLD  7963  resfunexgALT  7970  cofunexg  7971  fnexALT  7973  f1dmex  7979  oprabexd  7998  mpoexxg  8098  suppfnss  8212  tposexg  8263  tz7.48-3  8482  oaabs  8684  erex  8767  mapexOLD  8870  pmvalg  8875  elpmg  8881  elmapssres  8905  pmss12g  8907  ralxpmap  8934  ixpexg  8960  domssl  9036  ssdomg  9038  fiprc  9083  domunsncan  9110  infensuc  9193  pssnn  9206  ssfi  9211  enp1i  9310  unbnn  9329  fodomfi  9347  fodomfiOLD  9367  fival  9449  fiss  9461  dffi3  9468  hartogslem2  9580  card2on  9591  wdomima2g  9623  unxpwdom2  9625  unxpwdom  9626  harwdom  9628  oemapvali  9721  ackbij1lem11  10266  cofsmo  10306  ssfin4  10347  fin23lem11  10354  ssfin2  10357  ssfin3ds  10367  isfin1-3  10423  hsmex3  10471  axdc2lem  10485  ac6num  10516  ttukeylem1  10546  dmct  10561  ondomon  10600  fpwwe2lem3  10670  fpwwe2lem11  10678  fpwwe2lem12  10679  canthwe  10688  wuncss  10782  genpv  11036  genpdm  11039  hashss  14444  wrdexb  14559  shftfval  15105  o1of2  15645  o1rlimmul  15651  isercolllem2  15698  isstruct2  17182  ressval3d  17291  ressval3dOLD  17292  ressabs  17294  prdsbas  17503  fnmrc  17651  mrcfval  17652  isacs1i  17701  mreacs  17702  isssc  17867  ipolerval  18589  ress0g  18787  sylow2a  19651  islbs3  21174  toponsspwpw  22943  basdif0  22975  tgval  22977  eltg  22979  eltg2  22980  tgss  22990  basgen2  23011  2basgen  23012  bastop1  23015  topnex  23018  resttopon  23184  restabs  23188  restcld  23195  restfpw  23202  restcls  23204  restntr  23205  ordtbas2  23214  ordtbas  23215  lmfval  23255  cnrest  23308  cmpcov  23412  cmpsublem  23422  cmpsub  23423  2ndcomap  23481  islocfin  23540  txss12  23628  ptrescn  23662  trfbas2  23866  trfbas  23867  isfildlem  23880  snfbas  23889  trfil1  23909  trfil2  23910  trufil  23933  ssufl  23941  hauspwpwf1  24010  ustval  24226  metrest  24552  cnheibor  25000  metcld2  25354  bcthlem1  25371  mbfimaopn2  25705  0pledm  25721  dvbss  25950  dvreslem  25958  dvres2lem  25959  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcnvrelem2  26071  elply2  26249  plyf  26251  plyss  26252  elplyr  26254  plyeq0lem  26263  plyeq0  26264  plyaddlem  26268  plymullem  26269  dgrlem  26282  coeidlem  26290  ulmcn  26456  pserulm  26479  rabexgfGS  32526  abrexdomjm  32534  aciunf1  32679  ress1r  33223  pcmplfin  33820  metidval  33850  indval  33993  sigagenss  34129  measval  34178  omsfval  34275  omssubaddlem  34280  omssubadd  34281  carsggect  34299  erdsze2lem1  35187  erdsze2lem2  35188  cvxpconn  35226  elmsta  35532  dfon2lem3  35766  altxpexg  35959  ivthALT  36317  filnetlem3  36362  bj-sselpwuni  37032  bj-elpwg  37034  bj-restsnss  37065  bj-restsnss2  37066  bj-restb  37076  bj-restuni2  37080  abrexdom  37716  sdclem2  37728  sdclem1  37729  imaexALTV  38311  brssr  38482  sticksstones4  42130  sticksstones14  42141  pssexg  42243  elrfirn  42682  pwssplit4  43077  hbtlem1  43111  hbtlem7  43113  inaex  44292  rabexgf  44961  dvnprodlem2  45902  qndenserrnbllem  46249  sge0ss  46367  psmeasurelem  46425  caragensplit  46455  omeunile  46460  caragenuncl  46468  omeunle  46471  omeiunlempt  46475  carageniuncllem2  46477  fcdmvafv2v  47185  prprval  47438  mpoexxg2  48182  gsumlsscl  48224  lincellss  48271