Theorem ssexg 4732

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 3590	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 330	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3176	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 4730	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3239	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 445	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  ssexd  4733  difexg  4735  rabexg  4739  elssabg  4746  elpw2g  4754  abssexg  4777  snexALT  4778  sess1  5006  sess2  5007  riinint  5303  resexg  5362  trsuc  5727  ordsssuc2  5731  mptexg  6389  isofr2  6494  ofres  6811  brrpssg  6837  unexb  6856  xpexg  6858  difex2  6863  uniexb  6866  dmexg  6989  rnexg  6990  resiexg  6994  imaexg  6995  exse2  6998  cnvexg  7005  coexg  7010  fabexg  7015  f1oabexg  7018  resfunexgALT  7022  cofunexg  7023  fnexALT  7025  f1dmex  7029  oprabexd  7046  mpt2exxg  7133  suppfnss  7207  tposexg  7253  tz7.48-3  7426  oaabs  7611  erex  7653  mapex  7750  pmvalg  7755  elpmg  7759  elmapssres  7768  pmss12g  7770  ralxpmap  7793  ixpexg  7818  ssdomg  7887  fiprc  7924  domunsncan  7945  infensuc  8023  pssnn  8063  unbnn  8101  fodomfi  8124  fival  8201  fiss  8213  dffi3  8220  hartogslem2  8331  card2on  8342  wdomima2g  8374  unxpwdom2  8376  unxpwdom  8377  harwdom  8378  oemapvali  8464  ackbij1lem11  8935  cofsmo  8974  ssfin4  9015  fin23lem11  9022  ssfin2  9025  ssfin3ds  9035  isfin1-3  9091  hsmex3  9139  axdc2lem  9153  ac6num  9184  ttukeylem1  9214  ondomon  9264  fpwwe2lem3  9334  fpwwe2lem12  9342  fpwwe2lem13  9343  canthwe  9352  wuncss  9446  genpv  9700  genpdm  9703  hashss  13058  hashf1lem1  13096  wrdexg  13170  wrdexb  13171  shftfval  13658  o1of2  14191  o1rlimmul  14197  isercolllem2  14244  isstruct2  15704  ressval3d  15764  ressabs  15766  prdsbas  15940  fnmrc  16090  mrcfval  16091  isacs1i  16141  mreacs  16142  isssc  16303  ipolerval  16979  ress0g  17142  symgbas  17623  sylow2a  17857  islbs3  18976  basdif0  20568  tgval  20570  eltg  20572  eltg2  20573  tgss  20583  basgen2  20604  2basgen  20605  bastop1  20608  resttopon  20775  restabs  20779  restcld  20786  restfpw  20793  restcls  20795  restntr  20796  ordtbas2  20805  ordtbas  20806  lmfval  20846  cnrest  20899  cmpcov  21002  cmpsublem  21012  cmpsub  21013  2ndcomap  21071  islocfin  21130  txss12  21218  ptrescn  21252  trfbas2  21457  trfbas  21458  isfildlem  21471  snfbas  21480  trfil1  21500  trfil2  21501  trufil  21524  ssufl  21532  hauspwpwf1  21601  ustval  21816  metrest  22139  cnheibor  22562  metcld2  22913  bcthlem1  22929  mbfimaopn2  23230  0pledm  23246  dvbss  23471  dvreslem  23479  dvres2lem  23480  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvcnvrelem2  23585  elply2  23756  plyf  23758  plyss  23759  elplyr  23761  plyeq0lem  23770  plyeq0  23771  plyaddlem  23775  plymullem  23776  dgrlem  23789  coeidlem  23797  ulmcn  23957  pserulm  23980  iseupa  26492  rabexgfGS  28725  abrexdomjm  28729  mptexgf  28809  aciunf1  28845  dmct  28877  ress1r  29120  pcmplfin  29255  metidval  29261  indval  29403  sigagenss  29539  measval  29588  omsfval  29683  omssubaddlem  29688  omssubadd  29689  elcarsg  29694  carsggect  29707  erdsze2lem1  30439  erdsze2lem2  30440  cvxpcon  30478  elmsta  30699  dfon2lem3  30934  altxpexg  31255  ivthALT  31500  filnetlem3  31545  bj-restsnss  32217  bj-restsnss2  32218  bj-restb  32228  bj-restuni2  32232  bj-toponss  32241  bj-topnex  32247  abrexdom  32695  sdclem2  32708  sdclem1  32709  elrfirn  36276  pwssplit4  36677  hbtlem1  36712  hbtlem7  36714  rabexgf  38206  wessf1ornlem  38366  disjinfi  38375  dvnprodlem1  38836  dvnprodlem2  38837  qndenserrnbllem  39190  sge0ss  39305  psmeasurelem  39363  caragensplit  39390  omeunile  39395  caragenuncl  39403  omeunle  39406  omeiunlempt  39410  carageniuncllem2  39412  prcssprc  40306  mpt2exxg2  41909  gsumlsscl  41958  lincellss  42009