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 3964	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 343	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3460	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5279	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3524	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 411	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562   ∈ wcel 2144  Vcvv 3456   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923

This theorem is referenced by:  ssexd  5282  prcssprc  5285  difexg  5287  elpw2g  5291  rabexgOLD  5296  elssabg  5301  abssexg  5341  snexALT  5342  sess1  5614  sess2  5615  riinint  5950  resexg  6015  trsuc  6437  ordsssuc2  6441  mptexg  7207  mptexgf  7208  isofr2  7330  ofres  7681  brrpssg  7710  unexb  7732  unexbOLD  7733  xpexg  7735  abnexg  7741  difex2  7745  uniexr  7748  dmexg  7884  rnexg  7885  resiexg  7895  imaexg  7896  exse2  7900  cnvexg  7907  coexg  7912  resfunexgALT  7931  cofunexg  7932  fnexALT  7934  f1dmex  7940  oprabexd  7958  mpoexxg  8058  suppfnss  8171  tposexg  8222  tz7.48-3  8417  oaabs  8620  erex  8705  pmvalg  8820  elpmg  8826  elmapssres  8850  pmss12g  8853  ralxpmap  8880  ixpexg  8906  domssl  8981  ssdomg  8983  fiprc  9027  domunsncan  9051  infensuc  9129  pssnn  9139  ssfi  9143  enp1i  9225  unbnn  9242  fodomfi  9258  fival  9360  fiss  9372  dffi3  9379  hartogslem2  9493  card2on  9504  wdomima2g  9536  unxpwdom2  9538  unxpwdom  9539  harwdom  9541  oemapvali  9641  ackbij1lem11  10187  cofsmo  10228  ssfin4  10269  fin23lem11  10276  ssfin2  10279  ssfin3ds  10289  isfin1-3  10345  hsmex3  10393  axdc2lem  10407  ac6num  10438  ttukeylem1  10468  dmct  10483  fpwwe2lem3  10593  fpwwe2lem11  10601  fpwwe2lem12  10602  canthwe  10611  wuncss  10705  genpv  10959  genpdm  10962  indval  12200  hashss  14424  wrdexb  14540  shftfval  15085  o1of2  15642  o1rlimmul  15648  isercolllem2  15695  isstruct2  17187  ressval3d  17284  ressabs  17286  prdsbas  17488  fnmrc  17641  mrcfval  17642  isacs1i  17691  mreacs  17692  isssc  17855  ipolerval  18566  chnexg  18652  ress0g  18798  sylow2a  19661  islbs3  21227  toponsspwpw  22984  basdif0  23015  tgval  23017  eltg  23019  eltg2  23020  tgss  23030  basgen2  23051  2basgen  23052  bastop1  23055  topnex  23058  resttopon  23223  restabs  23227  restcld  23234  restfpw  23241  restcls  23243  restntr  23244  ordtbas2  23253  ordtbas  23254  lmfval  23294  cnrest  23347  cmpcov  23451  cmpsublem  23461  cmpsub  23462  2ndcomap  23520  islocfin  23579  txss12  23667  ptrescn  23701  trfbas2  23905  trfbas  23906  isfildlem  23919  snfbas  23928  trfil1  23948  trfil2  23949  trufil  23972  ssufl  23980  hauspwpwf1  24049  ustval  24265  metrest  24586  cnheibor  25019  metcld2  25371  bcthlem1  25388  mbfimaopn2  25721  0pledm  25737  dvbss  25965  dvreslem  25973  dvres2lem  25974  dvcnp2  25984  dvaddbr  26002  dvmulbr  26003  dvcnvrelem2  26082  elply2  26258  plyf  26260  plyss  26261  elplyr  26263  plyeq0lem  26272  plyeq0  26273  plyaddlem  26277  plymullem  26278  dgrlem  26291  coeidlem  26299  ulmcn  26464  pserulm  26487  rabexgfGS  32700  abrexdomjm  32708  aciunf1  32867  ress1r  33415  pcmplfin  34159  metidval  34189  sigagenss  34448  measval  34497  omsfval  34593  omssubaddlem  34598  omssubadd  34599  carsggect  34617  fineqvnttrclse  35424  erdsze2lem1  35558  erdsze2lem2  35559  cvxpconn  35597  elmsta  35903  dfon2lem3  36138  altxpexg  36333  ivthALT  36700  filnetlem3  36745  ttcexrg  36862  ttcsnexbig  36886  ttcexg  36897  bj-sselpwuni  37540  bj-elpwg  37542  bj-restsnss  37578  bj-restsnss2  37579  bj-restb  37589  bj-restuni2  37593  abrexdom  38234  sdclem2  38246  sdclem1  38247  brssr  39085  sticksstones4  42771  sticksstones14  42782  pssexg  42850  elrfirn  43281  pwssplit4  43671  hbtlem1  43705  hbtlem7  43707  inaex  44878  rabexgf  45609  dvnprodlem2  46526  qndenserrnbllem  46873  sge0ss  46991  psmeasurelem  47049  caragensplit  47079  omeunile  47084  caragenuncl  47092  omeunle  47095  omeiunlempt  47099  carageniuncllem2  47101  fcdmvafv2v  47835  prprval  48125  mpoexxg2  48965  gsumlsscl  49007  lincellss  49053  incat  50227