Theorem ssexg 5285

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 3973	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 341	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3450	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5283	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3526	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3446   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  ssexd  5286  prcssprc  5287  difexg  5289  rabexg  5293  elssabg  5298  elpw2g  5306  abssexg  5342  snexALT  5343  sess1  5606  sess2  5607  riinint  5928  resexg  5988  trsuc  6409  ordsssuc2  6413  mptexg  7176  mptexgf  7177  isofr2  7294  ofres  7641  brrpssg  7667  unexb  7687  xpexg  7689  abnexg  7695  difex2  7699  uniexr  7702  dmexg  7845  rnexg  7846  resiexg  7856  imaexg  7857  exse2  7859  cnvexg  7866  coexg  7871  fabexg  7876  f1oabexg  7878  resfunexgALT  7885  cofunexg  7886  fnexALT  7888  f1dmex  7894  oprabexd  7913  mpoexxg  8013  suppfnss  8125  tposexg  8176  tz7.48-3  8395  oaabs  8599  erex  8679  mapex  8778  pmvalg  8783  elpmg  8788  elmapssres  8812  pmss12g  8814  ralxpmap  8841  ixpexg  8867  domssl  8945  ssdomg  8947  fiprc  8996  domunsncan  9023  infensuc  9106  pssnn  9119  ssfi  9124  pssnnOLD  9216  enp1i  9230  unbnn  9250  fodomfi  9276  fival  9357  fiss  9369  dffi3  9376  hartogslem2  9488  card2on  9499  wdomima2g  9531  unxpwdom2  9533  unxpwdom  9534  harwdom  9536  oemapvali  9629  ackbij1lem11  10175  cofsmo  10214  ssfin4  10255  fin23lem11  10262  ssfin2  10265  ssfin3ds  10275  isfin1-3  10331  hsmex3  10379  axdc2lem  10393  ac6num  10424  ttukeylem1  10454  dmct  10469  ondomon  10508  fpwwe2lem3  10578  fpwwe2lem11  10586  fpwwe2lem12  10587  canthwe  10596  wuncss  10690  genpv  10944  genpdm  10947  hashss  14319  hashf1lem1OLD  14366  wrdexb  14425  shftfval  14967  o1of2  15507  o1rlimmul  15513  isercolllem2  15562  isstruct2  17032  ressval3d  17141  ressval3dOLD  17142  ressabs  17144  prdsbas  17353  fnmrc  17501  mrcfval  17502  isacs1i  17551  mreacs  17552  isssc  17717  ipolerval  18435  ress0g  18598  sylow2a  19415  islbs3  20675  toponsspwpw  22308  basdif0  22340  tgval  22342  eltg  22344  eltg2  22345  tgss  22355  basgen2  22376  2basgen  22377  bastop1  22380  topnex  22383  resttopon  22549  restabs  22553  restcld  22560  restfpw  22567  restcls  22569  restntr  22570  ordtbas2  22579  ordtbas  22580  lmfval  22620  cnrest  22673  cmpcov  22777  cmpsublem  22787  cmpsub  22788  2ndcomap  22846  islocfin  22905  txss12  22993  ptrescn  23027  trfbas2  23231  trfbas  23232  isfildlem  23245  snfbas  23254  trfil1  23274  trfil2  23275  trufil  23298  ssufl  23306  hauspwpwf1  23375  ustval  23591  metrest  23917  cnheibor  24355  metcld2  24708  bcthlem1  24725  mbfimaopn2  25058  0pledm  25074  dvbss  25302  dvreslem  25310  dvres2lem  25311  dvcnp2  25321  dvaddbr  25339  dvmulbr  25340  dvcnvrelem2  25419  elply2  25594  plyf  25596  plyss  25597  elplyr  25599  plyeq0lem  25608  plyeq0  25609  plyaddlem  25613  plymullem  25614  dgrlem  25627  coeidlem  25635  ulmcn  25795  pserulm  25818  rabexgfGS  31491  abrexdomjm  31497  aciunf1  31646  ress1r  32139  pcmplfin  32530  metidval  32560  indval  32701  sigagenss  32837  measval  32886  omsfval  32983  omssubaddlem  32988  omssubadd  32989  carsggect  33007  erdsze2lem1  33884  erdsze2lem2  33885  cvxpconn  33923  elmsta  34229  dfon2lem3  34446  altxpexg  34639  ivthALT  34883  filnetlem3  34928  bj-sselpwuni  35594  bj-elpwg  35596  bj-restsnss  35627  bj-restsnss2  35628  bj-restb  35638  bj-restuni2  35642  abrexdom  36262  sdclem2  36274  sdclem1  36275  imaexALTV  36864  brssr  37036  sticksstones4  40630  sticksstones14  40641  pssexg  40720  elrfirn  41076  pwssplit4  41474  hbtlem1  41508  hbtlem7  41510  inaex  42699  rabexgf  43351  dvnprodlem1  44307  dvnprodlem2  44308  qndenserrnbllem  44655  sge0ss  44773  psmeasurelem  44831  caragensplit  44861  omeunile  44866  caragenuncl  44874  omeunle  44877  omeiunlempt  44881  carageniuncllem2  44883  fcdmvafv2v  45588  prprval  45826  mpoexxg2  46533  gsumlsscl  46579  lincellss  46627