Theorem ssexg 5281

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  ssexd  5282  prcssprc  5285  difexg  5287  elpw2g  5291  rabexgOLD  5296  elssabg  5301  abssexg  5340  snexALT  5341  sess1  5606  sess2  5607  riinint  5938  resexg  6001  trsuc  6424  ordsssuc2  6428  mptexg  7198  mptexgf  7199  isofr2  7322  ofres  7675  brrpssg  7704  unexb  7726  unexbOLD  7727  xpexg  7729  abnexg  7735  difex2  7739  uniexr  7742  dmexg  7880  rnexg  7881  resiexg  7891  imaexg  7892  exse2  7896  cnvexg  7903  coexg  7908  fabexgOLD  7918  f1oabexgOLD  7922  resfunexgALT  7929  cofunexg  7930  fnexALT  7932  f1dmex  7938  oprabexd  7957  mpoexxg  8057  suppfnss  8171  tposexg  8222  tz7.48-3  8415  oaabs  8615  erex  8698  mapexOLD  8808  pmvalg  8813  elpmg  8819  elmapssres  8843  pmss12g  8845  ralxpmap  8872  ixpexg  8898  domssl  8972  ssdomg  8974  fiprc  9019  domunsncan  9046  infensuc  9125  pssnn  9138  ssfi  9143  enp1i  9231  unbnn  9250  fodomfi  9268  fodomfiOLD  9288  fival  9370  fiss  9382  dffi3  9389  hartogslem2  9503  card2on  9514  wdomima2g  9546  unxpwdom2  9548  unxpwdom  9549  harwdom  9551  oemapvali  9644  ackbij1lem11  10189  cofsmo  10229  ssfin4  10270  fin23lem11  10277  ssfin2  10280  ssfin3ds  10290  isfin1-3  10346  hsmex3  10394  axdc2lem  10408  ac6num  10439  ttukeylem1  10469  dmct  10484  ondomon  10523  fpwwe2lem3  10593  fpwwe2lem11  10601  fpwwe2lem12  10602  canthwe  10611  wuncss  10705  genpv  10959  genpdm  10962  hashss  14381  wrdexb  14497  shftfval  15043  o1of2  15586  o1rlimmul  15592  isercolllem2  15639  isstruct2  17126  ressval3d  17223  ressabs  17225  prdsbas  17427  fnmrc  17575  mrcfval  17576  isacs1i  17625  mreacs  17626  isssc  17789  ipolerval  18498  ress0g  18696  sylow2a  19556  islbs3  21072  toponsspwpw  22816  basdif0  22847  tgval  22849  eltg  22851  eltg2  22852  tgss  22862  basgen2  22883  2basgen  22884  bastop1  22887  topnex  22890  resttopon  23055  restabs  23059  restcld  23066  restfpw  23073  restcls  23075  restntr  23076  ordtbas2  23085  ordtbas  23086  lmfval  23126  cnrest  23179  cmpcov  23283  cmpsublem  23293  cmpsub  23294  2ndcomap  23352  islocfin  23411  txss12  23499  ptrescn  23533  trfbas2  23737  trfbas  23738  isfildlem  23751  snfbas  23760  trfil1  23780  trfil2  23781  trufil  23804  ssufl  23812  hauspwpwf1  23881  ustval  24097  metrest  24419  cnheibor  24861  metcld2  25214  bcthlem1  25231  mbfimaopn2  25565  0pledm  25581  dvbss  25809  dvreslem  25817  dvres2lem  25818  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcnvrelem2  25930  elply2  26108  plyf  26110  plyss  26111  elplyr  26113  plyeq0lem  26122  plyeq0  26123  plyaddlem  26127  plymullem  26128  dgrlem  26141  coeidlem  26149  ulmcn  26315  pserulm  26338  rabexgfGS  32435  abrexdomjm  32443  aciunf1  32594  indval  32783  ress1r  33192  pcmplfin  33857  metidval  33887  sigagenss  34146  measval  34195  omsfval  34292  omssubaddlem  34297  omssubadd  34298  carsggect  34316  erdsze2lem1  35197  erdsze2lem2  35198  cvxpconn  35236  elmsta  35542  dfon2lem3  35780  altxpexg  35973  ivthALT  36330  filnetlem3  36375  bj-sselpwuni  37045  bj-elpwg  37047  bj-restsnss  37078  bj-restsnss2  37079  bj-restb  37089  bj-restuni2  37093  abrexdom  37731  sdclem2  37743  sdclem1  37744  brssr  38499  sticksstones4  42144  sticksstones14  42155  pssexg  42221  elrfirn  42690  pwssplit4  43085  hbtlem1  43119  hbtlem7  43121  inaex  44293  rabexgf  45025  dvnprodlem2  45952  qndenserrnbllem  46299  sge0ss  46417  psmeasurelem  46475  caragensplit  46505  omeunile  46510  caragenuncl  46518  omeunle  46521  omeiunlempt  46525  carageniuncllem2  46527  fcdmvafv2v  47241  prprval  47519  mpoexxg2  48330  gsumlsscl  48372  lincellss  48419  incat  49594