Theorem ssexg 5006

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 3831	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 332	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3401	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5004	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3466	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 396	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ∈ wcel 2157  Vcvv 3398   ⊆ wss 3776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-in 3783  df-ss 3790

This theorem is referenced by:  ssexd  5007  prcssprc  5008  difexg  5010  rabexg  5013  elssabg  5018  elpw2g  5026  abssexg  5058  snexALT  5059  sess1  5286  sess2  5287  riinint  5590  resexg  5654  trsuc  6028  ordsssuc2  6032  mptexg  6712  mptexgf  6713  isofr2  6821  ofres  7146  brrpssg  7172  unexb  7191  xpexg  7193  abnexg  7197  difex2  7202  uniexr  7205  dmexg  7330  rnexg  7331  resiexg  7335  imaexg  7336  exse2  7338  cnvexg  7345  coexg  7350  fabexg  7355  f1oabexg  7358  resfunexgALT  7362  cofunexg  7363  fnexALT  7365  f1dmex  7369  oprabexd  7388  mpt2exxg  7480  suppfnss  7557  suppfnssOLD  7558  tposexg  7604  tz7.48-3  7778  oaabs  7964  erex  8006  mapex  8101  pmvalg  8106  elpmg  8111  elmapssres  8120  pmss12g  8122  ralxpmap  8147  ixpexg  8172  ssdomg  8241  fiprc  8281  domunsncan  8302  infensuc  8380  pssnn  8420  unbnn  8458  fodomfi  8481  fival  8560  fiss  8572  dffi3  8579  hartogslem2  8690  card2on  8701  wdomima2g  8733  unxpwdom2  8735  unxpwdom  8736  harwdom  8737  oemapvali  8831  ackbij1lem11  9340  cofsmo  9379  ssfin4  9420  fin23lem11  9427  ssfin2  9430  ssfin3ds  9440  isfin1-3  9496  hsmex3  9544  axdc2lem  9558  ac6num  9589  ttukeylem1  9619  dmct  9634  ondomon  9673  fpwwe2lem3  9743  fpwwe2lem12  9751  fpwwe2lem13  9752  canthwe  9761  wuncss  9855  genpv  10109  genpdm  10112  hashss  13417  hashf1lem1  13459  wrdexg  13529  wrdexb  13530  shftfval  14036  o1of2  14569  o1rlimmul  14575  isercolllem2  14622  isstruct2  16081  ressval3d  16151  ressval3dOLD  16152  ressabs  16154  prdsbas  16325  fnmrc  16475  mrcfval  16476  isacs1i  16525  mreacs  16526  isssc  16687  ipolerval  17364  ress0g  17527  symgbas  18004  sylow2a  18238  islbs3  19367  toponsspwpw  20944  basdif0  20975  tgval  20977  eltg  20979  eltg2  20980  tgss  20990  basgen2  21011  2basgen  21012  bastop1  21015  topnex  21018  resttopon  21183  restabs  21187  restcld  21194  restfpw  21201  restcls  21203  restntr  21204  ordtbas2  21213  ordtbas  21214  lmfval  21254  cnrest  21307  cmpcov  21410  cmpsublem  21420  cmpsub  21421  2ndcomap  21479  islocfin  21538  txss12  21626  ptrescn  21660  trfbas2  21864  trfbas  21865  isfildlem  21878  snfbas  21887  trfil1  21907  trfil2  21908  trufil  21931  ssufl  21939  hauspwpwf1  22008  ustval  22223  metrest  22546  cnheibor  22971  metcld2  23322  bcthlem1  23338  mbfimaopn2  23644  0pledm  23660  dvbss  23885  dvreslem  23893  dvres2lem  23894  dvcnp2  23903  dvaddbr  23921  dvmulbr  23922  dvcnvrelem2  24001  elply2  24172  plyf  24174  plyss  24175  elplyr  24177  plyeq0lem  24186  plyeq0  24187  plyaddlem  24191  plymullem  24192  dgrlem  24205  coeidlem  24213  ulmcn  24373  pserulm  24396  rabexgfGS  29671  abrexdomjm  29676  aciunf1  29796  ress1r  30120  pcmplfin  30258  metidval  30264  indval  30406  sigagenss  30543  measval  30592  omsfval  30687  omssubaddlem  30692  omssubadd  30693  elcarsg  30698  carsggect  30711  erdsze2lem1  31513  erdsze2lem2  31514  cvxpconn  31552  elmsta  31773  dfon2lem3  32015  altxpexg  32411  ivthALT  32656  filnetlem3  32701  bj-restsnss  33349  bj-restsnss2  33350  bj-restb  33360  bj-restuni2  33364  abrexdom  33839  sdclem2  33851  sdclem1  33852  brssr  34566  pssexg  37751  elrfirn  37761  pwssplit4  38161  hbtlem1  38195  hbtlem7  38197  rabexgf  39678  wessf1ornlem  39861  disjinfi  39870  dvnprodlem1  40642  dvnprodlem2  40643  qndenserrnbllem  40994  sge0ss  41109  psmeasurelem  41167  caragensplit  41197  omeunile  41202  caragenuncl  41210  omeunle  41213  omeiunlempt  41217  carageniuncllem2  41219  frnvafv2v  41826  mpt2exxg2  42685  gsumlsscl  42733  lincellss  42784