Theorem ssexg 5254

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 343	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3437	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5252	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3502	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 409	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885

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 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3892  df-ss 3902

This theorem is referenced by:  ssexd  5255  prcssprc  5258  difexg  5260  elpw2g  5264  rabexgOLD  5269  elssabg  5274  abssexg  5314  snexALT  5315  sess1  5586  sess2  5587  riinint  5921  resexg  5986  trsuc  6403  ordsssuc2  6407  mptexg  7169  mptexgf  7170  isofr2  7292  ofres  7643  brrpssg  7672  unexb  7694  unexbOLD  7695  xpexg  7697  abnexg  7703  difex2  7707  uniexr  7710  dmexg  7845  rnexg  7846  resiexg  7856  imaexg  7857  exse2  7861  cnvexg  7868  coexg  7873  fabexgOLD  7883  f1oabexgOLD  7887  resfunexgALT  7894  cofunexg  7895  fnexALT  7897  f1dmex  7903  oprabexd  7921  mpoexxg  8021  suppfnss  8133  tposexg  8184  tz7.48-3  8377  oaabs  8578  erex  8662  mapexOLD  8773  pmvalg  8778  elpmg  8784  elmapssres  8808  pmss12g  8811  ralxpmap  8838  ixpexg  8864  domssl  8939  ssdomg  8941  fiprc  8985  domunsncan  9009  infensuc  9087  pssnn  9097  ssfi  9101  enp1i  9183  unbnn  9200  fodomfi  9216  fodomfiOLD  9234  fival  9319  fiss  9331  dffi3  9338  hartogslem2  9452  card2on  9463  wdomima2g  9495  unxpwdom2  9497  unxpwdom  9498  harwdom  9500  oemapvali  9600  ackbij1lem11  10146  cofsmo  10186  ssfin4  10227  fin23lem11  10234  ssfin2  10237  ssfin3ds  10247  isfin1-3  10303  hsmex3  10351  axdc2lem  10365  ac6num  10396  ttukeylem1  10426  dmct  10441  fpwwe2lem3  10551  fpwwe2lem11  10559  fpwwe2lem12  10560  canthwe  10569  wuncss  10663  genpv  10917  genpdm  10920  indval  12157  hashss  14366  wrdexb  14482  shftfval  15027  o1of2  15570  o1rlimmul  15576  isercolllem2  15623  isstruct2  17114  ressval3d  17211  ressabs  17213  prdsbas  17415  fnmrc  17568  mrcfval  17569  isacs1i  17618  mreacs  17619  isssc  17782  ipolerval  18493  chnexg  18579  ress0g  18725  sylow2a  19589  islbs3  21152  toponsspwpw  22909  basdif0  22940  tgval  22942  eltg  22944  eltg2  22945  tgss  22955  basgen2  22976  2basgen  22977  bastop1  22980  topnex  22983  resttopon  23148  restabs  23152  restcld  23159  restfpw  23166  restcls  23168  restntr  23169  ordtbas2  23178  ordtbas  23179  lmfval  23219  cnrest  23272  cmpcov  23376  cmpsublem  23386  cmpsub  23387  2ndcomap  23445  islocfin  23504  txss12  23592  ptrescn  23626  trfbas2  23830  trfbas  23831  isfildlem  23844  snfbas  23853  trfil1  23873  trfil2  23874  trufil  23897  ssufl  23905  hauspwpwf1  23974  ustval  24190  metrest  24511  cnheibor  24944  metcld2  25296  bcthlem1  25313  mbfimaopn2  25646  0pledm  25662  dvbss  25890  dvreslem  25898  dvres2lem  25899  dvcnp2  25909  dvaddbr  25927  dvmulbr  25928  dvcnvrelem2  26007  elply2  26183  plyf  26185  plyss  26186  elplyr  26188  plyeq0lem  26197  plyeq0  26198  plyaddlem  26202  plymullem  26203  dgrlem  26216  coeidlem  26224  ulmcn  26386  pserulm  26409  rabexgfGS  32591  abrexdomjm  32599  aciunf1  32759  ress1r  33318  pcmplfin  34056  metidval  34086  sigagenss  34345  measval  34394  omsfval  34490  omssubaddlem  34495  omssubadd  34496  carsggect  34514  fineqvnttrclse  35320  erdsze2lem1  35446  erdsze2lem2  35447  cvxpconn  35485  elmsta  35791  dfon2lem3  36026  altxpexg  36221  ivthALT  36578  filnetlem3  36623  ttcexrg  36740  ttcsnexbig  36764  ttcexg  36775  bj-sselpwuni  37418  bj-elpwg  37420  bj-restsnss  37456  bj-restsnss2  37457  bj-restb  37467  bj-restuni2  37471  abrexdom  38112  sdclem2  38124  sdclem1  38125  brssr  38963  sticksstones4  42649  sticksstones14  42660  pssexg  42728  elrfirn  43159  pwssplit4  43549  hbtlem1  43583  hbtlem7  43585  inaex  44756  rabexgf  45487  dvnprodlem2  46404  qndenserrnbllem  46751  sge0ss  46869  psmeasurelem  46927  caragensplit  46957  omeunile  46962  caragenuncl  46970  omeunle  46973  omeiunlempt  46977  carageniuncllem2  46979  fcdmvafv2v  47713  prprval  48003  mpoexxg2  48843  gsumlsscl  48885  lincellss  48931  incat  50105