Theorem ssexg 5242

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ssexd  5243  prcssprc  5244  difexg  5246  rabexg  5250  elssabg  5255  elpw2g  5263  abssexg  5300  snexALT  5301  sess1  5548  sess2  5549  riinint  5866  resexg  5926  trsuc  6335  ordsssuc2  6339  mptexg  7079  mptexgf  7080  isofr2  7195  ofres  7530  brrpssg  7556  unexb  7576  xpexg  7578  abnexg  7584  difex2  7588  uniexr  7591  dmexg  7724  rnexg  7725  resiexg  7735  imaexg  7736  exse2  7738  cnvexg  7745  coexg  7750  fabexg  7755  f1oabexg  7757  resfunexgALT  7764  cofunexg  7765  fnexALT  7767  f1dmex  7773  oprabexd  7791  mpoexxg  7889  suppfnss  7976  tposexg  8027  tz7.48-3  8245  oaabs  8438  erex  8480  mapex  8579  pmvalg  8584  elpmg  8589  elmapssres  8613  pmss12g  8615  ralxpmap  8642  ixpexg  8668  ssdomg  8741  fiprc  8789  domunsncan  8812  infensuc  8891  pssnn  8913  ssfi  8918  pssnnOLD  8969  unbnn  9000  fodomfi  9022  fival  9101  fiss  9113  dffi3  9120  hartogslem2  9232  card2on  9243  wdomima2g  9275  unxpwdom2  9277  unxpwdom  9278  harwdom  9280  oemapvali  9372  ackbij1lem11  9917  cofsmo  9956  ssfin4  9997  fin23lem11  10004  ssfin2  10007  ssfin3ds  10017  isfin1-3  10073  hsmex3  10121  axdc2lem  10135  ac6num  10166  ttukeylem1  10196  dmct  10211  ondomon  10250  fpwwe2lem3  10320  fpwwe2lem11  10328  fpwwe2lem12  10329  canthwe  10338  wuncss  10432  genpv  10686  genpdm  10689  hashss  14052  hashf1lem1OLD  14097  wrdexb  14156  shftfval  14709  o1of2  15250  o1rlimmul  15256  isercolllem2  15305  isstruct2  16778  ressval3d  16882  ressval3dOLD  16883  ressabs  16885  prdsbas  17085  fnmrc  17233  mrcfval  17234  isacs1i  17283  mreacs  17284  isssc  17449  ipolerval  18165  ress0g  18328  sylow2a  19139  islbs3  20332  toponsspwpw  21979  basdif0  22011  tgval  22013  eltg  22015  eltg2  22016  tgss  22026  basgen2  22047  2basgen  22048  bastop1  22051  topnex  22054  resttopon  22220  restabs  22224  restcld  22231  restfpw  22238  restcls  22240  restntr  22241  ordtbas2  22250  ordtbas  22251  lmfval  22291  cnrest  22344  cmpcov  22448  cmpsublem  22458  cmpsub  22459  2ndcomap  22517  islocfin  22576  txss12  22664  ptrescn  22698  trfbas2  22902  trfbas  22903  isfildlem  22916  snfbas  22925  trfil1  22945  trfil2  22946  trufil  22969  ssufl  22977  hauspwpwf1  23046  ustval  23262  metrest  23586  cnheibor  24024  metcld2  24376  bcthlem1  24393  mbfimaopn2  24726  0pledm  24742  dvbss  24970  dvreslem  24978  dvres2lem  24979  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvcnvrelem2  25087  elply2  25262  plyf  25264  plyss  25265  elplyr  25267  plyeq0lem  25276  plyeq0  25277  plyaddlem  25281  plymullem  25282  dgrlem  25295  coeidlem  25303  ulmcn  25463  pserulm  25486  rabexgfGS  30747  abrexdomjm  30753  aciunf1  30902  ress1r  31388  pcmplfin  31712  metidval  31742  indval  31881  sigagenss  32017  measval  32066  omsfval  32161  omssubaddlem  32166  omssubadd  32167  carsggect  32185  erdsze2lem1  33065  erdsze2lem2  33066  cvxpconn  33104  elmsta  33410  dfon2lem3  33667  altxpexg  34207  ivthALT  34451  filnetlem3  34496  bj-sselpwuni  35150  bj-elpwg  35152  bj-restsnss  35181  bj-restsnss2  35182  bj-restb  35192  bj-restuni2  35196  abrexdom  35815  sdclem2  35827  sdclem1  35828  imaexALTV  36392  brssr  36546  sticksstones4  40033  sticksstones14  40044  pssexg  40127  elrfirn  40433  pwssplit4  40830  hbtlem1  40864  hbtlem7  40866  inaex  41804  rabexgf  42456  dvnprodlem1  43377  dvnprodlem2  43378  qndenserrnbllem  43725  sge0ss  43840  psmeasurelem  43898  caragensplit  43928  omeunile  43933  caragenuncl  43941  omeunle  43944  omeiunlempt  43948  carageniuncllem2  43950  frnvafv2v  44615  prprval  44854  mpoexxg2  45561  gsumlsscl  45607  lincellss  45655