Theorem ssexg 5280

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 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		inex2g 5279	. . 3 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ∩ 𝐵) ∈ V)
3		eleq1 2848	. . . 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 3450   ∩ cin 3897   ⊆ wss 3898

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 2732  ax-sep 5248

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3905  df-ss 3915

This theorem is used by:  ssex  5281  ssexd  5285  prcssprc  5288  difexg  5290  elpw2g  5294  elssabg  5303  abssexg  5343  snexALT  5344  sess1  5612  sess2  5613  riinint  5950  resexg  6014  trsuc  6441  ordsssuc2  6445  mptexg  7215  mptexgf  7216  isofr2  7340  ofres  7695  brrpssg  7724  unexb  7746  xpexg  7747  abnexg  7753  difex2  7757  uniexr  7760  dmexg  7896  rnexg  7897  resiexg  7907  imaexg  7908  exse2  7912  cnvexg  7919  coexg  7924  resfunexgALT  7943  cofunexg  7944  fnexALT  7946  f1dmex  7952  oprabexd  7970  mpoexxg  8071  suppfnss  8184  tposexg  8235  tz7.48-3  8432  oaabs  8635  erex  8720  pmvalg  8835  elpmg  8841  elmapssres  8872  pmss12g  8875  ralxpmap  8902  ixpexg  8928  domssl  9003  ssdomg  9005  fiprc  9050  domunsncan  9074  infensuc  9152  pssnn  9162  ssfi  9166  enp1i  9248  unbnn  9266  fodomfi  9282  fival  9382  fiss  9394  dffi3  9401  hartogslem2  9515  card2on  9526  wdomima2g  9558  unxpwdom2  9560  unxpwdom  9561  harwdom  9563  oemapvali  9663  ackbij1lem11  10278  cofsmo  10318  ssfin4  10359  fin23lem11  10366  ssfin2  10369  ssfin3ds  10379  isfin1-3  10435  hsmex3  10483  axdc2lem  10497  ac6num  10528  ttukeylem1  10558  dmctOLD  10574  fpwwe2lem3  10689  fpwwe2lem11  10697  fpwwe2lem12  10698  canthwe  10707  wuncss  10801  genpv  11055  genpdm  11058  indval  12292  hashss  14520  wrdexb  14637  shftfval  15190  o1of2  15747  o1rlimmul  15753  isercolllem2  15800  isstruct2  17288  ressval3d  17385  ressabs  17387  prdsbas  17589  fnmrc  17742  mrcfval  17743  isacs1i  17792  mreacs  17793  isssc  17956  ipolerval  18667  chnexg  18753  ress0gOLD  18916  sylow2a  19794  islbs3  21394  toponsspwpw  23201  basdif0  23232  tgval  23234  eltg  23236  eltg2  23237  tgss  23247  basgen2  23268  2basgen  23269  bastop1  23272  topnex  23275  resttopon  23440  restabs  23444  restcld  23451  restfpw  23458  restcls  23460  restntr  23461  ordtbas2  23470  ordtbas  23471  lmfval  23511  cnrest  23564  cmpcov  23668  cmpsublem  23678  cmpsub  23679  2ndcomap  23738  islocfin  23797  txss12  23885  ptrescn  23919  trfbas2  24123  trfbas  24124  isfildlem  24137  snfbas  24146  trfil1  24166  trfil2  24167  trufil  24190  ssufl  24198  hauspwpwf1  24267  ustval  24483  metrest  24804  cnheibor  25237  metcld2  25589  bcthlem1  25606  mbfimaopn2  25939  0pledm  25955  dvbss  26182  dvreslem  26190  dvres2lem  26191  dvcnp2  26201  dvaddbr  26219  dvmulbr  26220  dvcnvrelem2  26299  elply2  26475  plyf  26477  plyss  26478  elplyr  26480  plyeq0lem  26490  plyeq0  26491  plyaddlem  26495  plymullem  26496  dgrlem  26509  coeidlem  26517  ulmcn  26689  pserulm  26712  rabexgfGS  33028  abrexdomjm  33036  aciunf1  33190  ress1r  33726  pcmplfin  34425  metidval  34455  sigagenss  34715  measval  34764  omsfval  34860  omssubaddlem  34865  omssubadd  34866  carsggect  34884  fineqvnttrclse  35717  erdsze2lem1  35889  erdsze2lem2  35890  cvxpconn  35928  elmsta  36234  dfon2lem3  36469  altxpexg  36665  ivthALT  37045  filnetlem3  37090  ttcexrg  37207  ttcsnexbig  37231  ttcexg  37242  bj-sselpwuni  37885  bj-elpwg  37887  bj-restsnss  37924  bj-restsnss2  37925  bj-restb  37935  bj-restuni2  37939  abrexdom  38584  sdclem2  38596  sdclem1  38597  brssr  39433  sticksstones4  43119  sticksstones14  43130  pssexg  43200  elrfirn  43644  pwssplit4  44034  hbtlem1  44068  hbtlem7  44070  inaex  45225  rabexgf  45962  dvnprodlem2  46879  qndenserrnbllem  47226  sge0ss  47344  psmeasurelem  47402  caragensplit  47432  omeunile  47437  caragenuncl  47445  omeunle  47448  omeiunlempt  47452  carageniuncllem2  47454  fcdmvafv2v  48228  prprval  48518  mpoexxg2  49372  gsumlsscl  49414  lincellss  49460  incat  50631