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 4094	. 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 1569   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  ssex  5281  ssexd  5285  prcssprc  5288  difexg  5290  elpw2g  5294  elssabg  5303  abssexg  5343  snexALT  5344  sess1  5615  sess2  5616  riinint  5953  resexg  6015  trsuc  6452  ordsssuc2  6456  mptexg  7227  mptexgf  7228  isofr2  7352  ofres  7712  brrpssg  7741  unexb  7763  xpexg  7764  abnexg  7770  difex2  7774  uniexr  7777  dmexg  7913  rnexg  7914  resiexg  7924  imaexg  7925  exse2  7929  cnvexg  7936  coexg  7941  resfunexgALT  7960  cofunexg  7961  fnexALT  7963  f1dmex  7969  oprabexd  7987  mpoexxg  8088  suppfnss  8206  tposexg  8257  tz7.48-3  8454  oaabs  8657  erex  8742  pmvalg  8857  elpmg  8863  elmapssres  8894  pmss12g  8897  ralxpmap  8924  ixpexg  8950  domssl  9025  ssdomg  9027  fiprc  9072  domunsncan  9096  infensuc  9174  pssnn  9184  ssfi  9188  enp1i  9270  unbnn  9288  fodomfi  9304  fival  9404  fiss  9416  dffi3  9423  hartogslem2  9537  card2on  9548  wdomima2g  9580  unxpwdom2  9582  unxpwdom  9583  harwdom  9585  oemapvali  9685  ackbij1lem11  10307  cofsmo  10347  ssfin4  10388  fin23lem11  10395  ssfin2  10398  ssfin3ds  10408  isfin1-3  10464  hsmex3  10512  axdc2lem  10526  ac6num  10557  ttukeylem1  10587  dmctOLD  10603  fpwwe2lem3  10718  fpwwe2lem11  10726  fpwwe2lem12  10727  canthwe  10736  wuncss  10830  genpv  11084  genpdm  11087  indval  12323  hashss  14553  wrdexb  14670  shftfval  15223  o1of2  15780  o1rlimmul  15786  isercolllem2  15833  isstruct2  17327  ressval3d  17424  ressabs  17426  prdsbas  17628  fnmrc  17781  mrcfval  17782  isacs1i  17831  mreacs  17832  isssc  17995  ipolerval  18706  chnexg  18792  ress0gOLD  18955  sylow2a  19833  islbs3  21433  toponsspwpw  23240  basdif0  23271  tgval  23273  eltg  23275  eltg2  23276  tgss  23286  basgen2  23307  2basgen  23308  bastop1  23311  topnex  23314  resttopon  23479  restabs  23483  restcld  23490  restfpw  23497  restcls  23499  restntr  23500  ordtbas2  23509  ordtbas  23510  lmfval  23550  cnrest  23603  cmpcov  23707  cmpsublem  23717  cmpsub  23718  2ndcomap  23777  islocfin  23836  txss12  23924  ptrescn  23958  trfbas2  24162  trfbas  24163  isfildlem  24176  snfbas  24185  trfil1  24205  trfil2  24206  trufil  24229  ssufl  24237  hauspwpwf1  24306  ustval  24522  metrest  24843  cnheibor  25276  metcld2  25628  bcthlem1  25645  mbfimaopn2  25978  0pledm  25994  dvbss  26221  dvreslem  26229  dvres2lem  26230  dvcnp2  26240  dvaddbr  26258  dvmulbr  26259  dvcnvrelem2  26338  elply2  26514  plyf  26516  plyss  26517  elplyr  26519  plyeq0lem  26529  plyeq0  26530  plyaddlem  26534  plymullem  26535  dgrlem  26548  coeidlem  26556  ulmcn  26726  pserulm  26749  rabexgfGS  33095  abrexdomjm  33103  aciunf1  33257  ress1r  33793  pcmplfin  34492  metidval  34522  sigagenss  34782  measval  34831  omsfval  34926  omssubaddlem  34931  omssubadd  34932  carsggect  34950  abweex  35718  acwer1prc  35760  fineqvnttrclse  35792  erdsze2lem1  35968  erdsze2lem2  35969  cvxpconn  36007  elmsta  36313  dfon2lem3  36547  altxpexg  36743  ivthALT  37123  filnetlem3  37168  ttcexrg  37285  ttcsnexbig  37309  ttcexg  37320  bj-sselpwuni  37965  bj-elpwg  37967  bj-restsnss  38004  bj-restsnss2  38005  bj-restb  38015  bj-restuni2  38019  abrexdom  38665  sdclem2  38677  sdclem1  38678  brssr  39514  sticksstones4  43200  sticksstones14  43211  pssexg  43281  elrfirn  43706  pwssplit4  44091  hbtlem1  44125  hbtlem7  44127  inaex  45281  rabexgf  46041  dvnprodlem2  46957  qndenserrnbllem  47304  sge0ss  47422  psmeasurelem  47480  caragensplit  47510  omeunile  47515  caragenuncl  47523  omeunle  47526  omeiunlempt  47530  carageniuncllem2  47532  fcdmvafv2v  48306  prprval  48596  mpoexxg2  49450  gsumlsscl  49492  lincellss  49538  incat  50709