Theorem ssexg 4837

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 3660	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 330	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3234	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 4835	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3297	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 445	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  Vcvv 3231   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621

This theorem is referenced by:  ssexd  4838  prcssprc  4839  difexg  4841  rabexg  4844  elssabg  4849  elpw2g  4857  abssexg  4881  snexALT  4882  sess1  5111  sess2  5112  riinint  5414  resexg  5477  trsuc  5848  ordsssuc2  5852  mptexg  6525  mptexgf  6526  isofr2  6634  ofres  6955  brrpssg  6981  unexb  7000  xpexg  7002  abnexg  7006  difex2  7011  uniexr  7014  dmexg  7139  rnexg  7140  resiexg  7144  imaexg  7145  exse2  7147  cnvexg  7154  coexg  7159  fabexg  7164  f1oabexg  7167  resfunexgALT  7171  cofunexg  7172  fnexALT  7174  f1dmex  7178  oprabexd  7197  mpt2exxg  7289  suppfnss  7365  tposexg  7411  tz7.48-3  7584  oaabs  7769  erex  7811  mapex  7905  pmvalg  7910  elpmg  7915  elmapssres  7924  pmss12g  7926  ralxpmap  7949  ixpexg  7974  ssdomg  8043  fiprc  8080  domunsncan  8101  infensuc  8179  pssnn  8219  unbnn  8257  fodomfi  8280  fival  8359  fiss  8371  dffi3  8378  hartogslem2  8489  card2on  8500  wdomima2g  8532  unxpwdom2  8534  unxpwdom  8535  harwdom  8536  oemapvali  8619  ackbij1lem11  9090  cofsmo  9129  ssfin4  9170  fin23lem11  9177  ssfin2  9180  ssfin3ds  9190  isfin1-3  9246  hsmex3  9294  axdc2lem  9308  ac6num  9339  ttukeylem1  9369  dmct  9384  ondomon  9423  fpwwe2lem3  9493  fpwwe2lem12  9501  fpwwe2lem13  9502  canthwe  9511  wuncss  9605  genpv  9859  genpdm  9862  hashss  13235  hashf1lem1  13277  wrdexg  13347  wrdexb  13348  shftfval  13854  o1of2  14387  o1rlimmul  14393  isercolllem2  14440  isstruct2  15914  ressval3d  15984  ressabs  15986  prdsbas  16164  fnmrc  16314  mrcfval  16315  isacs1i  16365  mreacs  16366  isssc  16527  ipolerval  17203  ress0g  17366  symgbas  17846  sylow2a  18080  islbs3  19203  toponsspwpw  20774  basdif0  20805  tgval  20807  eltg  20809  eltg2  20810  tgss  20820  basgen2  20841  2basgen  20842  bastop1  20845  topnex  20848  resttopon  21013  restabs  21017  restcld  21024  restfpw  21031  restcls  21033  restntr  21034  ordtbas2  21043  ordtbas  21044  lmfval  21084  cnrest  21137  cmpcov  21240  cmpsublem  21250  cmpsub  21251  2ndcomap  21309  islocfin  21368  txss12  21456  ptrescn  21490  trfbas2  21694  trfbas  21695  isfildlem  21708  snfbas  21717  trfil1  21737  trfil2  21738  trufil  21761  ssufl  21769  hauspwpwf1  21838  ustval  22053  metrest  22376  cnheibor  22801  metcld2  23151  bcthlem1  23167  mbfimaopn2  23469  0pledm  23485  dvbss  23710  dvreslem  23718  dvres2lem  23719  dvcnp2  23728  dvaddbr  23746  dvmulbr  23747  dvcnvrelem2  23826  elply2  23997  plyf  23999  plyss  24000  elplyr  24002  plyeq0lem  24011  plyeq0  24012  plyaddlem  24016  plymullem  24017  dgrlem  24030  coeidlem  24038  ulmcn  24198  pserulm  24221  rabexgfGS  29466  abrexdomjm  29471  aciunf1  29591  ress1r  29917  pcmplfin  30055  metidval  30061  indval  30203  sigagenss  30340  measval  30389  omsfval  30484  omssubaddlem  30489  omssubadd  30490  elcarsg  30495  carsggect  30508  erdsze2lem1  31311  erdsze2lem2  31312  cvxpconn  31350  elmsta  31571  dfon2lem3  31814  altxpexg  32210  ivthALT  32455  filnetlem3  32500  bj-restsnss  33161  bj-restsnss2  33162  bj-restb  33172  bj-restuni2  33176  abrexdom  33655  sdclem2  33668  sdclem1  33669  brssr  34391  elrfirn  37575  pwssplit4  37976  hbtlem1  38010  hbtlem7  38012  rabexgf  39497  wessf1ornlem  39685  disjinfi  39694  dvnprodlem1  40479  dvnprodlem2  40480  qndenserrnbllem  40832  sge0ss  40947  psmeasurelem  41005  caragensplit  41035  omeunile  41040  caragenuncl  41048  omeunle  41051  omeiunlempt  41055  carageniuncllem2  41057  mpt2exxg2  42441  gsumlsscl  42489  lincellss  42540