Theorem ssexg 5269

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-in 3909  df-ss 3919

This theorem is referenced by:  ssexd  5270  prcssprc  5273  difexg  5275  elpw2g  5279  rabexgOLD  5284  elssabg  5289  abssexg  5328  snexALT  5329  sess1  5590  sess2  5591  riinint  5922  resexg  5987  trsuc  6407  ordsssuc2  6411  mptexg  7170  mptexgf  7171  isofr2  7293  ofres  7644  brrpssg  7673  unexb  7695  unexbOLD  7696  xpexg  7698  abnexg  7704  difex2  7708  uniexr  7711  dmexg  7846  rnexg  7847  resiexg  7857  imaexg  7858  exse2  7862  cnvexg  7869  coexg  7874  fabexgOLD  7884  f1oabexgOLD  7888  resfunexgALT  7895  cofunexg  7896  fnexALT  7898  f1dmex  7904  oprabexd  7922  mpoexxg  8022  suppfnss  8134  tposexg  8185  tz7.48-3  8378  oaabs  8579  erex  8663  mapexOLD  8774  pmvalg  8779  elpmg  8785  elmapssres  8809  pmss12g  8812  ralxpmap  8839  ixpexg  8865  domssl  8940  ssdomg  8942  fiprc  8986  domunsncan  9010  infensuc  9088  pssnn  9098  ssfi  9102  enp1i  9184  unbnn  9201  fodomfi  9217  fodomfiOLD  9235  fival  9320  fiss  9332  dffi3  9339  hartogslem2  9453  card2on  9464  wdomima2g  9496  unxpwdom2  9498  unxpwdom  9499  harwdom  9501  oemapvali  9598  ackbij1lem11  10144  cofsmo  10184  ssfin4  10225  fin23lem11  10232  ssfin2  10235  ssfin3ds  10245  isfin1-3  10301  hsmex3  10349  axdc2lem  10363  ac6num  10394  ttukeylem1  10424  dmct  10439  fpwwe2lem3  10549  fpwwe2lem11  10557  fpwwe2lem12  10558  canthwe  10567  wuncss  10661  genpv  10915  genpdm  10918  hashss  14337  wrdexb  14453  shftfval  14998  o1of2  15541  o1rlimmul  15547  isercolllem2  15594  isstruct2  17081  ressval3d  17178  ressabs  17180  prdsbas  17382  fnmrc  17535  mrcfval  17536  isacs1i  17585  mreacs  17586  isssc  17749  ipolerval  18460  chnexg  18546  ress0g  18692  sylow2a  19553  islbs3  21115  toponsspwpw  22871  basdif0  22902  tgval  22904  eltg  22906  eltg2  22907  tgss  22917  basgen2  22938  2basgen  22939  bastop1  22942  topnex  22945  resttopon  23110  restabs  23114  restcld  23121  restfpw  23128  restcls  23130  restntr  23131  ordtbas2  23140  ordtbas  23141  lmfval  23181  cnrest  23234  cmpcov  23338  cmpsublem  23348  cmpsub  23349  2ndcomap  23407  islocfin  23466  txss12  23554  ptrescn  23588  trfbas2  23792  trfbas  23793  isfildlem  23806  snfbas  23815  trfil1  23835  trfil2  23836  trufil  23859  ssufl  23867  hauspwpwf1  23936  ustval  24152  metrest  24473  cnheibor  24915  metcld2  25268  bcthlem1  25285  mbfimaopn2  25619  0pledm  25635  dvbss  25863  dvreslem  25871  dvres2lem  25872  dvcnp2  25882  dvcnp2OLD  25883  dvaddbr  25901  dvmulbr  25902  dvmulbrOLD  25903  dvcnvrelem2  25984  elply2  26162  plyf  26164  plyss  26165  elplyr  26167  plyeq0lem  26176  plyeq0  26177  plyaddlem  26181  plymullem  26182  dgrlem  26195  coeidlem  26203  ulmcn  26369  pserulm  26392  rabexgfGS  32578  abrexdomjm  32586  aciunf1  32745  indval  32935  ress1r  33319  pcmplfin  34030  metidval  34060  sigagenss  34319  measval  34368  omsfval  34464  omssubaddlem  34469  omssubadd  34470  carsggect  34488  fineqvnttrclse  35293  erdsze2lem1  35410  erdsze2lem2  35411  cvxpconn  35449  elmsta  35755  dfon2lem3  35990  altxpexg  36185  ivthALT  36542  filnetlem3  36587  bj-sselpwuni  37264  bj-elpwg  37266  bj-restsnss  37301  bj-restsnss2  37302  bj-restb  37312  bj-restuni2  37316  abrexdom  37944  sdclem2  37956  sdclem1  37957  brssr  38795  sticksstones4  42482  sticksstones14  42493  pssexg  42561  elrfirn  43015  pwssplit4  43409  hbtlem1  43443  hbtlem7  43445  inaex  44616  rabexgf  45347  dvnprodlem2  46268  qndenserrnbllem  46615  sge0ss  46733  psmeasurelem  46791  caragensplit  46821  omeunile  46826  caragenuncl  46834  omeunle  46837  omeiunlempt  46841  carageniuncllem2  46843  fcdmvafv2v  47559  prprval  47837  mpoexxg2  48661  gsumlsscl  48703  lincellss  48749  incat  49923