Theorem ssexg 5294

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 3969	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 344	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3465	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5292	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3529	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 412	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3461   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-in 3918  df-ss 3928

This theorem is referenced by:  ssexd  5295  prcssprc  5298  difexg  5300  elpw2g  5304  rabexgOLD  5309  elssabg  5314  abssexg  5354  snexALT  5355  sess1  5627  sess2  5628  riinint  5963  resexg  6027  trsuc  6451  ordsssuc2  6455  mptexg  7220  mptexgf  7221  isofr2  7343  ofres  7694  brrpssg  7723  unexb  7746  unexbOLD  7747  xpexg  7749  abnexg  7755  difex2  7759  uniexr  7762  dmexg  7898  rnexg  7899  resiexg  7909  imaexg  7910  exse2  7914  cnvexg  7921  coexg  7926  resfunexgALT  7945  cofunexg  7946  fnexALT  7948  f1dmex  7954  oprabexd  7972  mpoexxg  8072  suppfnss  8185  tposexg  8236  tz7.48-3  8431  oaabs  8634  erex  8719  pmvalg  8834  elpmg  8840  elmapssres  8864  pmss12g  8867  ralxpmap  8894  ixpexg  8920  domssl  8995  ssdomg  8997  fiprc  9041  domunsncan  9065  infensuc  9143  pssnn  9153  ssfi  9157  enp1i  9239  unbnn  9256  fodomfi  9272  fival  9372  fiss  9384  dffi3  9391  hartogslem2  9505  card2on  9516  wdomima2g  9548  unxpwdom2  9550  unxpwdom  9551  harwdom  9553  oemapvali  9653  ackbij1lem11  10212  cofsmo  10253  ssfin4  10294  fin23lem11  10301  ssfin2  10304  ssfin3ds  10314  isfin1-3  10370  hsmex3  10418  axdc2lem  10432  ac6num  10463  ttukeylem1  10493  dmct  10508  fpwwe2lem3  10618  fpwwe2lem11  10626  fpwwe2lem12  10627  canthwe  10636  wuncss  10730  genpv  10984  genpdm  10987  indval  12221  hashss  14445  wrdexb  14562  shftfval  15107  o1of2  15664  o1rlimmul  15670  isercolllem2  15717  isstruct2  17209  ressval3d  17306  ressabs  17308  prdsbas  17510  fnmrc  17663  mrcfval  17664  isacs1i  17713  mreacs  17714  isssc  17877  ipolerval  18588  chnexg  18674  ress0g  18820  sylow2a  19689  islbs3  21257  toponsspwpw  23048  basdif0  23079  tgval  23081  eltg  23083  eltg2  23084  tgss  23094  basgen2  23115  2basgen  23116  bastop1  23119  topnex  23122  resttopon  23287  restabs  23291  restcld  23298  restfpw  23305  restcls  23307  restntr  23308  ordtbas2  23317  ordtbas  23318  lmfval  23358  cnrest  23411  cmpcov  23515  cmpsublem  23525  cmpsub  23526  2ndcomap  23584  islocfin  23643  txss12  23731  ptrescn  23765  trfbas2  23969  trfbas  23970  isfildlem  23983  snfbas  23992  trfil1  24012  trfil2  24013  trufil  24036  ssufl  24044  hauspwpwf1  24113  ustval  24329  metrest  24650  cnheibor  25083  metcld2  25435  bcthlem1  25452  mbfimaopn2  25785  0pledm  25801  dvbss  26029  dvreslem  26037  dvres2lem  26038  dvcnp2  26048  dvaddbr  26066  dvmulbr  26067  dvcnvrelem2  26146  elply2  26322  plyf  26324  plyss  26325  elplyr  26327  plyeq0lem  26336  plyeq0  26337  plyaddlem  26341  plymullem  26342  dgrlem  26355  coeidlem  26363  ulmcn  26528  pserulm  26551  rabexgfGS  32786  abrexdomjm  32794  aciunf1  32949  ress1r  33493  pcmplfin  34195  metidval  34225  sigagenss  34484  measval  34533  omsfval  34629  omssubaddlem  34634  omssubadd  34635  carsggect  34653  fineqvnttrclse  35470  erdsze2lem1  35628  erdsze2lem2  35629  cvxpconn  35667  elmsta  35973  dfon2lem3  36208  altxpexg  36403  ivthALT  36769  filnetlem3  36814  ttcexrg  36931  ttcsnexbig  36955  ttcexg  36966  bj-sselpwuni  37609  bj-elpwg  37611  bj-restsnss  37648  bj-restsnss2  37649  bj-restb  37659  bj-restuni2  37663  abrexdom  38304  sdclem2  38316  sdclem1  38317  brssr  39155  sticksstones4  42841  sticksstones14  42852  pssexg  42922  elrfirn  43353  pwssplit4  43743  hbtlem1  43777  hbtlem7  43779  inaex  44934  rabexgf  45671  dvnprodlem2  46588  qndenserrnbllem  46935  sge0ss  47053  psmeasurelem  47111  caragensplit  47141  omeunile  47146  caragenuncl  47154  omeunle  47157  omeiunlempt  47161  carageniuncllem2  47163  fcdmvafv2v  47897  prprval  48187  mpoexxg2  49038  gsumlsscl  49080  lincellss  49126  incat  50299