Theorem ssexg 5272

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 3446	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5270	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3513	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  ssexd  5273  prcssprc  5276  difexg  5278  elpw2g  5282  rabexgOLD  5287  elssabg  5292  abssexg  5331  snexALT  5332  sess1  5599  sess2  5600  riinint  5931  resexg  5996  trsuc  6416  ordsssuc2  6420  mptexg  7179  mptexgf  7180  isofr2  7302  ofres  7653  brrpssg  7682  unexb  7704  unexbOLD  7705  xpexg  7707  abnexg  7713  difex2  7717  uniexr  7720  dmexg  7855  rnexg  7856  resiexg  7866  imaexg  7867  exse2  7871  cnvexg  7878  coexg  7883  fabexgOLD  7893  f1oabexgOLD  7897  resfunexgALT  7904  cofunexg  7905  fnexALT  7907  f1dmex  7913  oprabexd  7931  mpoexxg  8031  suppfnss  8143  tposexg  8194  tz7.48-3  8387  oaabs  8588  erex  8672  mapexOLD  8783  pmvalg  8788  elpmg  8794  elmapssres  8818  pmss12g  8821  ralxpmap  8848  ixpexg  8874  domssl  8949  ssdomg  8951  fiprc  8995  domunsncan  9019  infensuc  9097  pssnn  9107  ssfi  9111  enp1i  9193  unbnn  9210  fodomfi  9226  fodomfiOLD  9244  fival  9329  fiss  9341  dffi3  9348  hartogslem2  9462  card2on  9473  wdomima2g  9505  unxpwdom2  9507  unxpwdom  9508  harwdom  9510  oemapvali  9607  ackbij1lem11  10153  cofsmo  10193  ssfin4  10234  fin23lem11  10241  ssfin2  10244  ssfin3ds  10254  isfin1-3  10310  hsmex3  10358  axdc2lem  10372  ac6num  10403  ttukeylem1  10433  dmct  10448  fpwwe2lem3  10558  fpwwe2lem11  10566  fpwwe2lem12  10567  canthwe  10576  wuncss  10670  genpv  10924  genpdm  10927  hashss  14346  wrdexb  14462  shftfval  15007  o1of2  15550  o1rlimmul  15556  isercolllem2  15603  isstruct2  17090  ressval3d  17187  ressabs  17189  prdsbas  17391  fnmrc  17544  mrcfval  17545  isacs1i  17594  mreacs  17595  isssc  17758  ipolerval  18469  chnexg  18555  ress0g  18701  sylow2a  19565  islbs3  21127  toponsspwpw  22883  basdif0  22914  tgval  22916  eltg  22918  eltg2  22919  tgss  22929  basgen2  22950  2basgen  22951  bastop1  22954  topnex  22957  resttopon  23122  restabs  23126  restcld  23133  restfpw  23140  restcls  23142  restntr  23143  ordtbas2  23152  ordtbas  23153  lmfval  23193  cnrest  23246  cmpcov  23350  cmpsublem  23360  cmpsub  23361  2ndcomap  23419  islocfin  23478  txss12  23566  ptrescn  23600  trfbas2  23804  trfbas  23805  isfildlem  23818  snfbas  23827  trfil1  23847  trfil2  23848  trufil  23871  ssufl  23879  hauspwpwf1  23948  ustval  24164  metrest  24485  cnheibor  24927  metcld2  25280  bcthlem1  25297  mbfimaopn2  25631  0pledm  25647  dvbss  25875  dvreslem  25883  dvres2lem  25884  dvcnp2  25894  dvcnp2OLD  25895  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvcnvrelem2  25996  elply2  26174  plyf  26176  plyss  26177  elplyr  26179  plyeq0lem  26188  plyeq0  26189  plyaddlem  26193  plymullem  26194  dgrlem  26207  coeidlem  26215  ulmcn  26381  pserulm  26404  rabexgfGS  32592  abrexdomjm  32600  aciunf1  32759  indval  32949  ress1r  33333  pcmplfin  34044  metidval  34074  sigagenss  34333  measval  34382  omsfval  34478  omssubaddlem  34483  omssubadd  34484  carsggect  34502  fineqvnttrclse  35308  erdsze2lem1  35425  erdsze2lem2  35426  cvxpconn  35464  elmsta  35770  dfon2lem3  36005  altxpexg  36200  ivthALT  36557  filnetlem3  36602  bj-sselpwuni  37325  bj-elpwg  37327  bj-restsnss  37363  bj-restsnss2  37364  bj-restb  37374  bj-restuni2  37378  abrexdom  38010  sdclem2  38022  sdclem1  38023  brssr  38861  sticksstones4  42548  sticksstones14  42559  pssexg  42627  elrfirn  43081  pwssplit4  43475  hbtlem1  43509  hbtlem7  43511  inaex  44682  rabexgf  45413  dvnprodlem2  46334  qndenserrnbllem  46681  sge0ss  46799  psmeasurelem  46857  caragensplit  46887  omeunile  46892  caragenuncl  46900  omeunle  46903  omeiunlempt  46907  carageniuncllem2  46909  fcdmvafv2v  47625  prprval  47903  mpoexxg2  48727  gsumlsscl  48769  lincellss  48815  incat  49989