Theorem ssexg 5259

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 3956	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 341	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3440	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5257	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3507	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  ssexd  5260  prcssprc  5263  difexg  5265  elpw2g  5269  rabexgOLD  5274  elssabg  5279  abssexg  5318  snexALT  5319  sess1  5579  sess2  5580  riinint  5910  resexg  5975  trsuc  6395  ordsssuc2  6399  mptexg  7155  mptexgf  7156  isofr2  7278  ofres  7629  brrpssg  7658  unexb  7680  unexbOLD  7681  xpexg  7683  abnexg  7689  difex2  7693  uniexr  7696  dmexg  7831  rnexg  7832  resiexg  7842  imaexg  7843  exse2  7847  cnvexg  7854  coexg  7859  fabexgOLD  7869  f1oabexgOLD  7873  resfunexgALT  7880  cofunexg  7881  fnexALT  7883  f1dmex  7889  oprabexd  7907  mpoexxg  8007  suppfnss  8119  tposexg  8170  tz7.48-3  8363  oaabs  8563  erex  8646  mapexOLD  8756  pmvalg  8761  elpmg  8767  elmapssres  8791  pmss12g  8793  ralxpmap  8820  ixpexg  8846  domssl  8920  ssdomg  8922  fiprc  8966  domunsncan  8990  infensuc  9068  pssnn  9078  ssfi  9082  enp1i  9163  unbnn  9180  fodomfi  9196  fodomfiOLD  9214  fival  9296  fiss  9308  dffi3  9315  hartogslem2  9429  card2on  9440  wdomima2g  9472  unxpwdom2  9474  unxpwdom  9475  harwdom  9477  oemapvali  9574  ackbij1lem11  10120  cofsmo  10160  ssfin4  10201  fin23lem11  10208  ssfin2  10211  ssfin3ds  10221  isfin1-3  10277  hsmex3  10325  axdc2lem  10339  ac6num  10370  ttukeylem1  10400  dmct  10415  ondomon  10454  fpwwe2lem3  10524  fpwwe2lem11  10532  fpwwe2lem12  10533  canthwe  10542  wuncss  10636  genpv  10890  genpdm  10893  hashss  14316  wrdexb  14432  shftfval  14977  o1of2  15520  o1rlimmul  15526  isercolllem2  15573  isstruct2  17060  ressval3d  17157  ressabs  17159  prdsbas  17361  fnmrc  17513  mrcfval  17514  isacs1i  17563  mreacs  17564  isssc  17727  ipolerval  18438  chnexg  18524  ress0g  18670  sylow2a  19531  islbs3  21092  toponsspwpw  22837  basdif0  22868  tgval  22870  eltg  22872  eltg2  22873  tgss  22883  basgen2  22904  2basgen  22905  bastop1  22908  topnex  22911  resttopon  23076  restabs  23080  restcld  23087  restfpw  23094  restcls  23096  restntr  23097  ordtbas2  23106  ordtbas  23107  lmfval  23147  cnrest  23200  cmpcov  23304  cmpsublem  23314  cmpsub  23315  2ndcomap  23373  islocfin  23432  txss12  23520  ptrescn  23554  trfbas2  23758  trfbas  23759  isfildlem  23772  snfbas  23781  trfil1  23801  trfil2  23802  trufil  23825  ssufl  23833  hauspwpwf1  23902  ustval  24118  metrest  24439  cnheibor  24881  metcld2  25234  bcthlem1  25251  mbfimaopn2  25585  0pledm  25601  dvbss  25829  dvreslem  25837  dvres2lem  25838  dvcnp2  25848  dvcnp2OLD  25849  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcnvrelem2  25950  elply2  26128  plyf  26130  plyss  26131  elplyr  26133  plyeq0lem  26142  plyeq0  26143  plyaddlem  26147  plymullem  26148  dgrlem  26161  coeidlem  26169  ulmcn  26335  pserulm  26358  rabexgfGS  32479  abrexdomjm  32487  aciunf1  32645  indval  32834  ress1r  33201  pcmplfin  33873  metidval  33903  sigagenss  34162  measval  34211  omsfval  34307  omssubaddlem  34312  omssubadd  34313  carsggect  34331  fineqvnttrclse  35144  erdsze2lem1  35247  erdsze2lem2  35248  cvxpconn  35286  elmsta  35592  dfon2lem3  35827  altxpexg  36022  ivthALT  36379  filnetlem3  36424  bj-sselpwuni  37094  bj-elpwg  37096  bj-restsnss  37127  bj-restsnss2  37128  bj-restb  37138  bj-restuni2  37142  abrexdom  37769  sdclem2  37781  sdclem1  37782  brssr  38592  sticksstones4  42241  sticksstones14  42252  pssexg  42318  elrfirn  42787  pwssplit4  43181  hbtlem1  43215  hbtlem7  43217  inaex  44389  rabexgf  45120  dvnprodlem2  46044  qndenserrnbllem  46391  sge0ss  46509  psmeasurelem  46567  caragensplit  46597  omeunile  46602  caragenuncl  46610  omeunle  46613  omeiunlempt  46617  carageniuncllem2  46619  fcdmvafv2v  47335  prprval  47613  mpoexxg2  48437  gsumlsscl  48479  lincellss  48526  incat  49701