Theorem ssexg 5253

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

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

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 2707  ax-sep 5220

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 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-in 3892  df-ss 3902

This theorem is referenced by:  ssexd  5254  prcssprc  5257  difexg  5259  elpw2g  5263  rabexgOLD  5268  elssabg  5273  abssexg  5313  snexALT  5314  sess1  5585  sess2  5586  riinint  5916  resexg  5981  trsuc  6401  ordsssuc2  6405  mptexg  7165  mptexgf  7166  isofr2  7288  ofres  7639  brrpssg  7668  unexb  7690  unexbOLD  7691  xpexg  7693  abnexg  7699  difex2  7703  uniexr  7706  dmexg  7841  rnexg  7842  resiexg  7852  imaexg  7853  exse2  7857  cnvexg  7864  coexg  7869  fabexgOLD  7879  f1oabexgOLD  7883  resfunexgALT  7890  cofunexg  7891  fnexALT  7893  f1dmex  7899  oprabexd  7917  mpoexxg  8017  suppfnss  8128  tposexg  8179  tz7.48-3  8372  oaabs  8573  erex  8657  mapexOLD  8768  pmvalg  8773  elpmg  8779  elmapssres  8803  pmss12g  8806  ralxpmap  8833  ixpexg  8859  domssl  8934  ssdomg  8936  fiprc  8980  domunsncan  9004  infensuc  9082  pssnn  9092  ssfi  9096  enp1i  9178  unbnn  9195  fodomfi  9211  fodomfiOLD  9229  fival  9314  fiss  9326  dffi3  9333  hartogslem2  9447  card2on  9458  wdomima2g  9490  unxpwdom2  9492  unxpwdom  9493  harwdom  9495  oemapvali  9594  ackbij1lem11  10140  cofsmo  10180  ssfin4  10221  fin23lem11  10228  ssfin2  10231  ssfin3ds  10241  isfin1-3  10297  hsmex3  10345  axdc2lem  10359  ac6num  10390  ttukeylem1  10420  dmct  10435  fpwwe2lem3  10545  fpwwe2lem11  10553  fpwwe2lem12  10554  canthwe  10563  wuncss  10657  genpv  10911  genpdm  10914  indval  12151  hashss  14360  wrdexb  14476  shftfval  15021  o1of2  15564  o1rlimmul  15570  isercolllem2  15617  isstruct2  17108  ressval3d  17205  ressabs  17207  prdsbas  17409  fnmrc  17562  mrcfval  17563  isacs1i  17612  mreacs  17613  isssc  17776  ipolerval  18487  chnexg  18573  ress0g  18719  sylow2a  19583  islbs3  21142  toponsspwpw  22875  basdif0  22906  tgval  22908  eltg  22910  eltg2  22911  tgss  22921  basgen2  22942  2basgen  22943  bastop1  22946  topnex  22949  resttopon  23114  restabs  23118  restcld  23125  restfpw  23132  restcls  23134  restntr  23135  ordtbas2  23144  ordtbas  23145  lmfval  23185  cnrest  23238  cmpcov  23342  cmpsublem  23352  cmpsub  23353  2ndcomap  23411  islocfin  23470  txss12  23558  ptrescn  23592  trfbas2  23796  trfbas  23797  isfildlem  23810  snfbas  23819  trfil1  23839  trfil2  23840  trufil  23863  ssufl  23871  hauspwpwf1  23940  ustval  24156  metrest  24477  cnheibor  24910  metcld2  25262  bcthlem1  25279  mbfimaopn2  25612  0pledm  25628  dvbss  25856  dvreslem  25864  dvres2lem  25865  dvcnp2  25875  dvaddbr  25893  dvmulbr  25894  dvcnvrelem2  25973  elply2  26149  plyf  26151  plyss  26152  elplyr  26154  plyeq0lem  26163  plyeq0  26164  plyaddlem  26168  plymullem  26169  dgrlem  26182  coeidlem  26190  ulmcn  26352  pserulm  26375  rabexgfGS  32557  abrexdomjm  32565  aciunf1  32724  ress1r  33282  pcmplfin  33992  metidval  34022  sigagenss  34281  measval  34330  omsfval  34426  omssubaddlem  34431  omssubadd  34432  carsggect  34450  fineqvnttrclse  35256  erdsze2lem1  35373  erdsze2lem2  35374  cvxpconn  35412  elmsta  35718  dfon2lem3  35953  altxpexg  36148  ivthALT  36505  filnetlem3  36550  ttcexrg  36667  ttcsnexbig  36691  ttcexg  36702  bj-sselpwuni  37345  bj-elpwg  37347  bj-restsnss  37383  bj-restsnss2  37384  bj-restb  37394  bj-restuni2  37398  abrexdom  38039  sdclem2  38051  sdclem1  38052  brssr  38890  sticksstones4  42576  sticksstones14  42587  pssexg  42655  elrfirn  43115  pwssplit4  43505  hbtlem1  43539  hbtlem7  43541  inaex  44712  rabexgf  45443  dvnprodlem2  46363  qndenserrnbllem  46710  sge0ss  46828  psmeasurelem  46886  caragensplit  46916  omeunile  46921  caragenuncl  46929  omeunle  46932  omeiunlempt  46936  carageniuncllem2  46938  fcdmvafv2v  47672  prprval  47962  mpoexxg2  48802  gsumlsscl  48844  lincellss  48890  incat  50064