Theorem ssexg 5278

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 3451	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5276	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3520	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  ssexd  5279  prcssprc  5282  difexg  5284  elpw2g  5288  rabexgOLD  5293  elssabg  5298  abssexg  5337  snexALT  5338  sess1  5603  sess2  5604  riinint  5935  resexg  5998  trsuc  6421  ordsssuc2  6425  mptexg  7195  mptexgf  7196  isofr2  7319  ofres  7672  brrpssg  7701  unexb  7723  unexbOLD  7724  xpexg  7726  abnexg  7732  difex2  7736  uniexr  7739  dmexg  7877  rnexg  7878  resiexg  7888  imaexg  7889  exse2  7893  cnvexg  7900  coexg  7905  fabexgOLD  7915  f1oabexgOLD  7919  resfunexgALT  7926  cofunexg  7927  fnexALT  7929  f1dmex  7935  oprabexd  7954  mpoexxg  8054  suppfnss  8168  tposexg  8219  tz7.48-3  8412  oaabs  8612  erex  8695  mapexOLD  8805  pmvalg  8810  elpmg  8816  elmapssres  8840  pmss12g  8842  ralxpmap  8869  ixpexg  8895  domssl  8969  ssdomg  8971  fiprc  9016  domunsncan  9041  infensuc  9119  pssnn  9132  ssfi  9137  enp1i  9224  unbnn  9243  fodomfi  9261  fodomfiOLD  9281  fival  9363  fiss  9375  dffi3  9382  hartogslem2  9496  card2on  9507  wdomima2g  9539  unxpwdom2  9541  unxpwdom  9542  harwdom  9544  oemapvali  9637  ackbij1lem11  10182  cofsmo  10222  ssfin4  10263  fin23lem11  10270  ssfin2  10273  ssfin3ds  10283  isfin1-3  10339  hsmex3  10387  axdc2lem  10401  ac6num  10432  ttukeylem1  10462  dmct  10477  ondomon  10516  fpwwe2lem3  10586  fpwwe2lem11  10594  fpwwe2lem12  10595  canthwe  10604  wuncss  10698  genpv  10952  genpdm  10955  hashss  14374  wrdexb  14490  shftfval  15036  o1of2  15579  o1rlimmul  15585  isercolllem2  15632  isstruct2  17119  ressval3d  17216  ressabs  17218  prdsbas  17420  fnmrc  17568  mrcfval  17569  isacs1i  17618  mreacs  17619  isssc  17782  ipolerval  18491  ress0g  18689  sylow2a  19549  islbs3  21065  toponsspwpw  22809  basdif0  22840  tgval  22842  eltg  22844  eltg2  22845  tgss  22855  basgen2  22876  2basgen  22877  bastop1  22880  topnex  22883  resttopon  23048  restabs  23052  restcld  23059  restfpw  23066  restcls  23068  restntr  23069  ordtbas2  23078  ordtbas  23079  lmfval  23119  cnrest  23172  cmpcov  23276  cmpsublem  23286  cmpsub  23287  2ndcomap  23345  islocfin  23404  txss12  23492  ptrescn  23526  trfbas2  23730  trfbas  23731  isfildlem  23744  snfbas  23753  trfil1  23773  trfil2  23774  trufil  23797  ssufl  23805  hauspwpwf1  23874  ustval  24090  metrest  24412  cnheibor  24854  metcld2  25207  bcthlem1  25224  mbfimaopn2  25558  0pledm  25574  dvbss  25802  dvreslem  25810  dvres2lem  25811  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcnvrelem2  25923  elply2  26101  plyf  26103  plyss  26104  elplyr  26106  plyeq0lem  26115  plyeq0  26116  plyaddlem  26120  plymullem  26121  dgrlem  26134  coeidlem  26142  ulmcn  26308  pserulm  26331  rabexgfGS  32428  abrexdomjm  32436  aciunf1  32587  indval  32776  ress1r  33185  pcmplfin  33850  metidval  33880  sigagenss  34139  measval  34188  omsfval  34285  omssubaddlem  34290  omssubadd  34291  carsggect  34309  erdsze2lem1  35190  erdsze2lem2  35191  cvxpconn  35229  elmsta  35535  dfon2lem3  35773  altxpexg  35966  ivthALT  36323  filnetlem3  36368  bj-sselpwuni  37038  bj-elpwg  37040  bj-restsnss  37071  bj-restsnss2  37072  bj-restb  37082  bj-restuni2  37086  abrexdom  37724  sdclem2  37736  sdclem1  37737  brssr  38492  sticksstones4  42137  sticksstones14  42148  pssexg  42214  elrfirn  42683  pwssplit4  43078  hbtlem1  43112  hbtlem7  43114  inaex  44286  rabexgf  45018  dvnprodlem2  45945  qndenserrnbllem  46292  sge0ss  46410  psmeasurelem  46468  caragensplit  46498  omeunile  46503  caragenuncl  46511  omeunle  46514  omeiunlempt  46518  carageniuncllem2  46520  fcdmvafv2v  47237  prprval  47515  mpoexxg2  48326  gsumlsscl  48368  lincellss  48415  incat  49590