Theorem ssexg 5324

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 4009	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 340	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3476	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5322	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3541	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  Vcvv 3472   ⊆ wss 3949

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3956  df-ss 3966

This theorem is referenced by:  ssexd  5325  prcssprc  5326  difexg  5328  rabexg  5332  elssabg  5337  elpw2g  5345  abssexg  5381  snexALT  5382  sess1  5645  sess2  5646  riinint  5968  resexg  6028  trsuc  6452  ordsssuc2  6456  mptexg  7226  mptexgf  7227  isofr2  7345  ofres  7693  brrpssg  7719  unexb  7739  xpexg  7741  abnexg  7747  difex2  7751  uniexr  7754  dmexg  7898  rnexg  7899  resiexg  7909  imaexg  7910  exse2  7912  cnvexg  7919  coexg  7924  fabexg  7929  f1oabexg  7931  resfunexgALT  7938  cofunexg  7939  fnexALT  7941  f1dmex  7947  oprabexd  7966  mpoexxg  8066  suppfnss  8178  tposexg  8229  tz7.48-3  8448  oaabs  8651  erex  8731  mapex  8830  pmvalg  8835  elpmg  8841  elmapssres  8865  pmss12g  8867  ralxpmap  8894  ixpexg  8920  domssl  8998  ssdomg  9000  fiprc  9049  domunsncan  9076  infensuc  9159  pssnn  9172  ssfi  9177  pssnnOLD  9269  enp1i  9283  unbnn  9303  fodomfi  9329  fival  9411  fiss  9423  dffi3  9430  hartogslem2  9542  card2on  9553  wdomima2g  9585  unxpwdom2  9587  unxpwdom  9588  harwdom  9590  oemapvali  9683  ackbij1lem11  10229  cofsmo  10268  ssfin4  10309  fin23lem11  10316  ssfin2  10319  ssfin3ds  10329  isfin1-3  10385  hsmex3  10433  axdc2lem  10447  ac6num  10478  ttukeylem1  10508  dmct  10523  ondomon  10562  fpwwe2lem3  10632  fpwwe2lem11  10640  fpwwe2lem12  10641  canthwe  10650  wuncss  10744  genpv  10998  genpdm  11001  hashss  14375  hashf1lem1OLD  14422  wrdexb  14481  shftfval  15023  o1of2  15563  o1rlimmul  15569  isercolllem2  15618  isstruct2  17088  ressval3d  17197  ressval3dOLD  17198  ressabs  17200  prdsbas  17409  fnmrc  17557  mrcfval  17558  isacs1i  17607  mreacs  17608  isssc  17773  ipolerval  18491  ress0g  18689  sylow2a  19530  islbs3  20915  toponsspwpw  22646  basdif0  22678  tgval  22680  eltg  22682  eltg2  22683  tgss  22693  basgen2  22714  2basgen  22715  bastop1  22718  topnex  22721  resttopon  22887  restabs  22891  restcld  22898  restfpw  22905  restcls  22907  restntr  22908  ordtbas2  22917  ordtbas  22918  lmfval  22958  cnrest  23011  cmpcov  23115  cmpsublem  23125  cmpsub  23126  2ndcomap  23184  islocfin  23243  txss12  23331  ptrescn  23365  trfbas2  23569  trfbas  23570  isfildlem  23583  snfbas  23592  trfil1  23612  trfil2  23613  trufil  23636  ssufl  23644  hauspwpwf1  23713  ustval  23929  metrest  24255  cnheibor  24703  metcld2  25057  bcthlem1  25074  mbfimaopn2  25408  0pledm  25424  dvbss  25652  dvreslem  25660  dvres2lem  25661  dvcnp2  25671  dvaddbr  25689  dvmulbr  25690  dvcnvrelem2  25769  elply2  25944  plyf  25946  plyss  25947  elplyr  25949  plyeq0lem  25958  plyeq0  25959  plyaddlem  25963  plymullem  25964  dgrlem  25977  coeidlem  25985  ulmcn  26145  pserulm  26168  rabexgfGS  32004  abrexdomjm  32009  aciunf1  32153  ress1r  32651  pcmplfin  33136  metidval  33166  indval  33307  sigagenss  33443  measval  33492  omsfval  33589  omssubaddlem  33594  omssubadd  33595  carsggect  33613  erdsze2lem1  34490  erdsze2lem2  34491  cvxpconn  34529  elmsta  34835  dfon2lem3  35059  altxpexg  35252  gg-dvcnp2  35462  gg-dvmulbr  35463  ivthALT  35525  filnetlem3  35570  bj-sselpwuni  36236  bj-elpwg  36238  bj-restsnss  36269  bj-restsnss2  36270  bj-restb  36280  bj-restuni2  36284  abrexdom  36903  sdclem2  36915  sdclem1  36916  imaexALTV  37504  brssr  37676  sticksstones4  41273  sticksstones14  41284  pssexg  41352  elrfirn  41737  pwssplit4  42135  hbtlem1  42169  hbtlem7  42171  inaex  43360  rabexgf  44012  dvnprodlem1  44962  dvnprodlem2  44963  qndenserrnbllem  45310  sge0ss  45428  psmeasurelem  45486  caragensplit  45516  omeunile  45521  caragenuncl  45529  omeunle  45532  omeiunlempt  45536  carageniuncllem2  45538  fcdmvafv2v  46244  prprval  46482  mpoexxg2  47103  gsumlsscl  47149  lincellss  47196