Theorem ssexg 5201

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 3913	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 345	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3402	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5199	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3471	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 411	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  Vcvv 3398   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  ssexd  5202  prcssprc  5203  difexg  5205  rabexg  5209  elssabg  5214  elpw2g  5222  abssexg  5260  snexALT  5261  sess1  5504  sess2  5505  riinint  5822  resexg  5882  trsuc  6275  ordsssuc2  6279  mptexg  7015  mptexgf  7016  isofr2  7131  ofres  7465  brrpssg  7491  unexb  7511  xpexg  7513  abnexg  7519  difex2  7523  uniexr  7526  dmexg  7659  rnexg  7660  resiexg  7670  imaexg  7671  exse2  7673  cnvexg  7680  coexg  7685  fabexg  7690  f1oabexg  7692  resfunexgALT  7699  cofunexg  7700  fnexALT  7702  f1dmex  7708  oprabexd  7726  mpoexxg  7824  suppfnss  7909  tposexg  7960  tz7.48-3  8158  oaabs  8351  erex  8393  mapex  8492  pmvalg  8497  elpmg  8502  elmapssres  8526  pmss12g  8528  ralxpmap  8555  ixpexg  8581  ssdomg  8652  fiprc  8700  domunsncan  8723  infensuc  8802  pssnn  8824  ssfi  8829  pssnnOLD  8872  unbnn  8905  fodomfi  8927  fival  9006  fiss  9018  dffi3  9025  hartogslem2  9137  card2on  9148  wdomima2g  9180  unxpwdom2  9182  unxpwdom  9183  harwdom  9185  oemapvali  9277  ackbij1lem11  9809  cofsmo  9848  ssfin4  9889  fin23lem11  9896  ssfin2  9899  ssfin3ds  9909  isfin1-3  9965  hsmex3  10013  axdc2lem  10027  ac6num  10058  ttukeylem1  10088  dmct  10103  ondomon  10142  fpwwe2lem3  10212  fpwwe2lem11  10220  fpwwe2lem12  10221  canthwe  10230  wuncss  10324  genpv  10578  genpdm  10581  hashss  13941  hashf1lem1OLD  13986  wrdexb  14045  shftfval  14598  o1of2  15139  o1rlimmul  15145  isercolllem2  15194  isstruct2  16676  ressval3d  16745  ressabs  16747  prdsbas  16916  fnmrc  17064  mrcfval  17065  isacs1i  17114  mreacs  17115  isssc  17279  ipolerval  17992  ress0g  18155  sylow2a  18962  islbs3  20146  toponsspwpw  21773  basdif0  21804  tgval  21806  eltg  21808  eltg2  21809  tgss  21819  basgen2  21840  2basgen  21841  bastop1  21844  topnex  21847  resttopon  22012  restabs  22016  restcld  22023  restfpw  22030  restcls  22032  restntr  22033  ordtbas2  22042  ordtbas  22043  lmfval  22083  cnrest  22136  cmpcov  22240  cmpsublem  22250  cmpsub  22251  2ndcomap  22309  islocfin  22368  txss12  22456  ptrescn  22490  trfbas2  22694  trfbas  22695  isfildlem  22708  snfbas  22717  trfil1  22737  trfil2  22738  trufil  22761  ssufl  22769  hauspwpwf1  22838  ustval  23054  metrest  23376  cnheibor  23806  metcld2  24158  bcthlem1  24175  mbfimaopn2  24508  0pledm  24524  dvbss  24752  dvreslem  24760  dvres2lem  24761  dvcnp2  24771  dvaddbr  24789  dvmulbr  24790  dvcnvrelem2  24869  elply2  25044  plyf  25046  plyss  25047  elplyr  25049  plyeq0lem  25058  plyeq0  25059  plyaddlem  25063  plymullem  25064  dgrlem  25077  coeidlem  25085  ulmcn  25245  pserulm  25268  rabexgfGS  30519  abrexdomjm  30525  aciunf1  30674  ress1r  31159  pcmplfin  31478  metidval  31508  indval  31647  sigagenss  31783  measval  31832  omsfval  31927  omssubaddlem  31932  omssubadd  31933  carsggect  31951  erdsze2lem1  32832  erdsze2lem2  32833  cvxpconn  32871  elmsta  33177  dfon2lem3  33431  altxpexg  33966  ivthALT  34210  filnetlem3  34255  bj-sselpwuni  34909  bj-elpwg  34911  bj-restsnss  34938  bj-restsnss2  34939  bj-restb  34949  bj-restuni2  34953  abrexdom  35574  sdclem2  35586  sdclem1  35587  imaexALTV  36151  brssr  36305  sticksstones4  39774  sticksstones14  39785  pssexg  39855  elrfirn  40161  pwssplit4  40558  hbtlem1  40592  hbtlem7  40594  inaex  41529  rabexgf  42181  dvnprodlem1  43105  dvnprodlem2  43106  qndenserrnbllem  43453  sge0ss  43568  psmeasurelem  43626  caragensplit  43656  omeunile  43661  caragenuncl  43669  omeunle  43672  omeiunlempt  43676  carageniuncllem2  43678  frnvafv2v  44343  prprval  44582  mpoexxg2  45289  gsumlsscl  45335  lincellss  45383