Theorem ssexg 5288

Description: A subclass of a set is a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) (Proof shortened by BJ, 18-Jul-2026.)

Assertion

Ref	Expression
ssexg	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Proof of Theorem ssexg

Step	Hyp	Ref	Expression
1		dfss2 3920	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		inex2g 5287	. . 3 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ∩ 𝐵) ∈ V)
3		eleq1 2850	. . . 4 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
4	3	biimpa 482	. . 3 ⊢ (((𝐴 ∩ 𝐵) = 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ V) → 𝐴 ∈ V)
5	2, 4	sylan2 605	. 2 ⊢ (((𝐴 ∩ 𝐵) = 𝐴 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
6	1, 5	sylanb 593	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3453   ∩ cin 3901   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  ssex  5289  ssexd  5293  prcssprc  5296  difexg  5298  elpw2g  5302  elssabg  5311  abssexg  5351  snexALT  5352  sess1  5624  sess2  5625  riinint  5960  resexg  6024  trsuc  6451  ordsssuc2  6455  mptexg  7223  mptexgf  7224  isofr2  7348  ofres  7700  brrpssg  7729  unexb  7751  xpexg  7752  abnexg  7758  difex2  7762  uniexr  7765  dmexg  7901  rnexg  7902  resiexg  7912  imaexg  7913  exse2  7917  cnvexg  7924  coexg  7929  resfunexgALT  7948  cofunexg  7949  fnexALT  7951  f1dmex  7957  oprabexd  7975  mpoexxg  8077  suppfnss  8190  tposexg  8241  tz7.48-3  8436  oaabs  8639  erex  8724  pmvalg  8839  elpmg  8845  elmapssres  8876  pmss12g  8879  ralxpmap  8906  ixpexg  8932  domssl  9007  ssdomg  9009  fiprc  9054  domunsncan  9078  infensuc  9156  pssnn  9166  ssfi  9170  enp1i  9252  unbnn  9269  fodomfi  9285  fival  9385  fiss  9397  dffi3  9404  hartogslem2  9518  card2on  9529  wdomima2g  9561  unxpwdom2  9563  unxpwdom  9564  harwdom  9566  oemapvali  9666  ackbij1lem11  10234  cofsmo  10274  ssfin4  10315  fin23lem11  10322  ssfin2  10325  ssfin3ds  10335  isfin1-3  10391  hsmex3  10439  axdc2lem  10453  ac6num  10484  ttukeylem1  10514  dmctOLD  10530  fpwwe2lem3  10645  fpwwe2lem11  10653  fpwwe2lem12  10654  canthwe  10663  wuncss  10757  genpv  11011  genpdm  11014  indval  12248  hashss  14475  wrdexb  14592  shftfval  15145  o1of2  15702  o1rlimmul  15708  isercolllem2  15755  isstruct2  17245  ressval3d  17342  ressabs  17344  prdsbas  17546  fnmrc  17699  mrcfval  17700  isacs1i  17749  mreacs  17750  isssc  17913  ipolerval  18624  chnexg  18710  ress0gOLD  18870  sylow2a  19747  islbs3  21343  toponsspwpw  23148  basdif0  23179  tgval  23181  eltg  23183  eltg2  23184  tgss  23194  basgen2  23215  2basgen  23216  bastop1  23219  topnex  23222  resttopon  23387  restabs  23391  restcld  23398  restfpw  23405  restcls  23407  restntr  23408  ordtbas2  23417  ordtbas  23418  lmfval  23458  cnrest  23511  cmpcov  23615  cmpsublem  23625  cmpsub  23626  2ndcomap  23685  islocfin  23744  txss12  23832  ptrescn  23866  trfbas2  24070  trfbas  24071  isfildlem  24084  snfbas  24093  trfil1  24113  trfil2  24114  trufil  24137  ssufl  24145  hauspwpwf1  24214  ustval  24430  metrest  24751  cnheibor  25184  metcld2  25536  bcthlem1  25553  mbfimaopn2  25886  0pledm  25902  dvbss  26130  dvreslem  26138  dvres2lem  26139  dvcnp2  26149  dvaddbr  26167  dvmulbr  26168  dvcnvrelem2  26247  elply2  26423  plyf  26425  plyss  26426  elplyr  26428  plyeq0lem  26437  plyeq0  26438  plyaddlem  26442  plymullem  26443  dgrlem  26456  coeidlem  26464  ulmcn  26632  pserulm  26655  rabexgfGS  32960  abrexdomjm  32968  aciunf1  33123  ress1r  33659  pcmplfin  34357  metidval  34387  sigagenss  34647  measval  34696  omsfval  34792  omssubaddlem  34797  omssubadd  34798  carsggect  34816  fineqvnttrclse  35637  erdsze2lem1  35769  erdsze2lem2  35770  cvxpconn  35808  elmsta  36114  dfon2lem3  36349  altxpexg  36545  ivthALT  36941  filnetlem3  36986  ttcexrg  37103  ttcsnexbig  37127  ttcexg  37138  bj-sselpwuni  37781  bj-elpwg  37783  bj-restsnss  37820  bj-restsnss2  37821  bj-restb  37831  bj-restuni2  37835  abrexdom  38467  sdclem2  38479  sdclem1  38480  brssr  39316  sticksstones4  43002  sticksstones14  43013  pssexg  43083  elrfirn  43527  pwssplit4  43917  hbtlem1  43951  hbtlem7  43953  inaex  45108  rabexgf  45845  dvnprodlem2  46762  qndenserrnbllem  47109  sge0ss  47227  psmeasurelem  47285  caragensplit  47315  omeunile  47320  caragenuncl  47328  omeunle  47331  omeiunlempt  47335  carageniuncllem2  47337  fcdmvafv2v  48111  prprval  48401  mpoexxg2  49255  gsumlsscl  49297  lincellss  49343  incat  50514