Theorem ssexg 4804

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 3627	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 331	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3203	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 4802	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3266	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 446	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  ssexd  4805  prcssprc  4806  difexg  4808  rabexg  4812  elssabg  4819  elpw2g  4827  abssexg  4851  snexALT  4852  sess1  5082  sess2  5083  riinint  5382  resexg  5442  trsuc  5810  ordsssuc2  5814  mptexg  6484  mptexgf  6485  isofr2  6594  ofres  6913  brrpssg  6939  unexb  6958  xpexg  6960  abnexg  6964  difex2  6969  uniexr  6972  dmexg  7097  rnexg  7098  resiexg  7102  imaexg  7103  exse2  7105  cnvexg  7112  coexg  7117  fabexg  7122  f1oabexg  7125  resfunexgALT  7129  cofunexg  7130  fnexALT  7132  f1dmex  7136  oprabexd  7155  mpt2exxg  7244  suppfnss  7320  tposexg  7366  tz7.48-3  7539  oaabs  7724  erex  7766  mapex  7863  pmvalg  7868  elpmg  7873  elmapssres  7882  pmss12g  7884  ralxpmap  7907  ixpexg  7932  ssdomg  8001  fiprc  8039  domunsncan  8060  infensuc  8138  pssnn  8178  unbnn  8216  fodomfi  8239  fival  8318  fiss  8330  dffi3  8337  hartogslem2  8448  card2on  8459  wdomima2g  8491  unxpwdom2  8493  unxpwdom  8494  harwdom  8495  oemapvali  8581  ackbij1lem11  9052  cofsmo  9091  ssfin4  9132  fin23lem11  9139  ssfin2  9142  ssfin3ds  9152  isfin1-3  9208  hsmex3  9256  axdc2lem  9270  ac6num  9301  ttukeylem1  9331  dmct  9346  ondomon  9385  fpwwe2lem3  9455  fpwwe2lem12  9463  fpwwe2lem13  9464  canthwe  9473  wuncss  9567  genpv  9821  genpdm  9824  hashss  13197  hashf1lem1  13239  wrdexg  13315  wrdexb  13316  shftfval  13810  o1of2  14343  o1rlimmul  14349  isercolllem2  14396  isstruct2  15867  ressval3d  15937  ressabs  15939  prdsbas  16117  fnmrc  16267  mrcfval  16268  isacs1i  16318  mreacs  16319  isssc  16480  ipolerval  17156  ress0g  17319  symgbas  17800  sylow2a  18034  islbs3  19155  toponsspwpw  20726  basdif0  20757  tgval  20759  eltg  20761  eltg2  20762  tgss  20772  basgen2  20793  2basgen  20794  bastop1  20797  topnex  20800  resttopon  20965  restabs  20969  restcld  20976  restfpw  20983  restcls  20985  restntr  20986  ordtbas2  20995  ordtbas  20996  lmfval  21036  cnrest  21089  cmpcov  21192  cmpsublem  21202  cmpsub  21203  2ndcomap  21261  islocfin  21320  txss12  21408  ptrescn  21442  trfbas2  21647  trfbas  21648  isfildlem  21661  snfbas  21670  trfil1  21690  trfil2  21691  trufil  21714  ssufl  21722  hauspwpwf1  21791  ustval  22006  metrest  22329  cnheibor  22754  metcld2  23105  bcthlem1  23121  mbfimaopn2  23424  0pledm  23440  dvbss  23665  dvreslem  23673  dvres2lem  23674  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvcnvrelem2  23781  elply2  23952  plyf  23954  plyss  23955  elplyr  23957  plyeq0lem  23966  plyeq0  23967  plyaddlem  23971  plymullem  23972  dgrlem  23985  coeidlem  23993  ulmcn  24153  pserulm  24176  rabexgfGS  29340  abrexdomjm  29345  aciunf1  29463  ress1r  29789  pcmplfin  29927  metidval  29933  indval  30075  sigagenss  30212  measval  30261  omsfval  30356  omssubaddlem  30361  omssubadd  30362  elcarsg  30367  carsggect  30380  erdsze2lem1  31185  erdsze2lem2  31186  cvxpconn  31224  elmsta  31445  dfon2lem3  31690  altxpexg  32085  ivthALT  32330  filnetlem3  32375  bj-restsnss  33036  bj-restsnss2  33037  bj-restb  33047  bj-restuni2  33051  abrexdom  33525  sdclem2  33538  sdclem1  33539  elrfirn  37258  pwssplit4  37659  hbtlem1  37693  hbtlem7  37695  rabexgf  39183  wessf1ornlem  39371  disjinfi  39380  dvnprodlem1  40161  dvnprodlem2  40162  qndenserrnbllem  40514  sge0ss  40629  psmeasurelem  40687  caragensplit  40714  omeunile  40719  caragenuncl  40727  omeunle  40730  omeiunlempt  40734  carageniuncllem2  40736  mpt2exxg2  42116  gsumlsscl  42164  lincellss  42215