Theorem ssexg 5251

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 3952	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 342	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3435	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5249	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3504	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542   ∈ wcel 2110  Vcvv 3431   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  ssexd  5252  prcssprc  5253  difexg  5255  rabexg  5259  elssabg  5264  elpw2g  5272  abssexg  5309  snexALT  5310  sess1  5558  sess2  5559  riinint  5876  resexg  5936  trsuc  6349  ordsssuc2  6353  mptexg  7094  mptexgf  7095  isofr2  7211  ofres  7546  brrpssg  7572  unexb  7592  xpexg  7594  abnexg  7600  difex2  7604  uniexr  7607  dmexg  7744  rnexg  7745  resiexg  7755  imaexg  7756  exse2  7758  cnvexg  7765  coexg  7770  fabexg  7775  f1oabexg  7777  resfunexgALT  7784  cofunexg  7785  fnexALT  7787  f1dmex  7793  oprabexd  7811  mpoexxg  7909  suppfnss  7996  tposexg  8047  tz7.48-3  8266  oaabs  8461  erex  8505  mapex  8604  pmvalg  8609  elpmg  8614  elmapssres  8638  pmss12g  8640  ralxpmap  8667  ixpexg  8693  ssdomg  8769  fiprc  8818  domunsncan  8841  infensuc  8924  pssnn  8933  ssfi  8938  pssnnOLD  9018  unbnn  9048  fodomfi  9070  fival  9149  fiss  9161  dffi3  9168  hartogslem2  9280  card2on  9291  wdomima2g  9323  unxpwdom2  9325  unxpwdom  9326  harwdom  9328  oemapvali  9420  ackbij1lem11  9987  cofsmo  10026  ssfin4  10067  fin23lem11  10074  ssfin2  10077  ssfin3ds  10087  isfin1-3  10143  hsmex3  10191  axdc2lem  10205  ac6num  10236  ttukeylem1  10266  dmct  10281  ondomon  10320  fpwwe2lem3  10390  fpwwe2lem11  10398  fpwwe2lem12  10399  canthwe  10408  wuncss  10502  genpv  10756  genpdm  10759  hashss  14122  hashf1lem1OLD  14167  wrdexb  14226  shftfval  14779  o1of2  15320  o1rlimmul  15326  isercolllem2  15375  isstruct2  16848  ressval3d  16954  ressval3dOLD  16955  ressabs  16957  prdsbas  17166  fnmrc  17314  mrcfval  17315  isacs1i  17364  mreacs  17365  isssc  17530  ipolerval  18248  ress0g  18411  sylow2a  19222  islbs3  20415  toponsspwpw  22069  basdif0  22101  tgval  22103  eltg  22105  eltg2  22106  tgss  22116  basgen2  22137  2basgen  22138  bastop1  22141  topnex  22144  resttopon  22310  restabs  22314  restcld  22321  restfpw  22328  restcls  22330  restntr  22331  ordtbas2  22340  ordtbas  22341  lmfval  22381  cnrest  22434  cmpcov  22538  cmpsublem  22548  cmpsub  22549  2ndcomap  22607  islocfin  22666  txss12  22754  ptrescn  22788  trfbas2  22992  trfbas  22993  isfildlem  23006  snfbas  23015  trfil1  23035  trfil2  23036  trufil  23059  ssufl  23067  hauspwpwf1  23136  ustval  23352  metrest  23678  cnheibor  24116  metcld2  24469  bcthlem1  24486  mbfimaopn2  24819  0pledm  24835  dvbss  25063  dvreslem  25071  dvres2lem  25072  dvcnp2  25082  dvaddbr  25100  dvmulbr  25101  dvcnvrelem2  25180  elply2  25355  plyf  25357  plyss  25358  elplyr  25360  plyeq0lem  25369  plyeq0  25370  plyaddlem  25374  plymullem  25375  dgrlem  25388  coeidlem  25396  ulmcn  25556  pserulm  25579  rabexgfGS  30842  abrexdomjm  30848  aciunf1  30996  ress1r  31482  pcmplfin  31806  metidval  31836  indval  31977  sigagenss  32113  measval  32162  omsfval  32257  omssubaddlem  32262  omssubadd  32263  carsggect  32281  erdsze2lem1  33161  erdsze2lem2  33162  cvxpconn  33200  elmsta  33506  dfon2lem3  33757  altxpexg  34276  ivthALT  34520  filnetlem3  34565  bj-sselpwuni  35219  bj-elpwg  35221  bj-restsnss  35250  bj-restsnss2  35251  bj-restb  35261  bj-restuni2  35265  abrexdom  35884  sdclem2  35896  sdclem1  35897  imaexALTV  36461  brssr  36615  sticksstones4  40102  sticksstones14  40113  pssexg  40198  elrfirn  40514  pwssplit4  40911  hbtlem1  40945  hbtlem7  40947  inaex  41885  rabexgf  42537  dvnprodlem1  43458  dvnprodlem2  43459  qndenserrnbllem  43806  sge0ss  43921  psmeasurelem  43979  caragensplit  44009  omeunile  44014  caragenuncl  44022  omeunle  44025  omeiunlempt  44029  carageniuncllem2  44031  frnvafv2v  44696  prprval  44935  mpoexxg2  45642  gsumlsscl  45688  lincellss  45736