Theorem ssexg 5289

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 3922	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		inex2g 5288	. . 3 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ∩ 𝐵) ∈ V)
3		eleq1 2850	. . . 4 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V))
4	3	biimpa 481	. . 3 ⊢ (((𝐴 ∩ 𝐵) = 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ V) → 𝐴 ∈ V)
5	2, 4	sylan2 604	. 2 ⊢ (((𝐴 ∩ 𝐵) = 𝐴 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
6	1, 5	sylanb 592	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ∈ wcel 2142  Vcvv 3454   ∩ cin 3903   ⊆ wss 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921

This theorem is used by:  ssex  5290  ssexd  5294  prcssprc  5297  difexg  5299  elpw2g  5303  elssabg  5312  abssexg  5352  snexALT  5353  sess1  5625  sess2  5626  riinint  5961  resexg  6025  trsuc  6450  ordsssuc2  6454  mptexg  7219  mptexgf  7220  isofr2  7342  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  8070  suppfnss  8183  tposexg  8234  tz7.48-3  8429  oaabs  8632  erex  8717  pmvalg  8832  elpmg  8838  elmapssres  8862  pmss12g  8865  ralxpmap  8892  ixpexg  8918  domssl  8993  ssdomg  8995  fiprc  9039  domunsncan  9063  infensuc  9141  pssnn  9151  ssfi  9155  enp1i  9237  unbnn  9254  fodomfi  9270  fival  9370  fiss  9382  dffi3  9389  hartogslem2  9503  card2on  9514  wdomima2g  9546  unxpwdom2  9548  unxpwdom  9549  harwdom  9551  oemapvali  9651  ackbij1lem11  10219  cofsmo  10259  ssfin4  10300  fin23lem11  10307  ssfin2  10310  ssfin3ds  10320  isfin1-3  10376  hsmex3  10424  axdc2lem  10438  ac6num  10469  ttukeylem1  10499  dmct  10514  fpwwe2lem3  10624  fpwwe2lem11  10632  fpwwe2lem12  10633  canthwe  10642  wuncss  10736  genpv  10990  genpdm  10993  indval  12227  hashss  14452  wrdexb  14569  shftfval  15114  o1of2  15671  o1rlimmul  15677  isercolllem2  15724  isstruct2  17215  ressval3d  17312  ressabs  17314  prdsbas  17516  fnmrc  17669  mrcfval  17670  isacs1i  17719  mreacs  17720  isssc  17883  ipolerval  18594  chnexg  18680  ress0g  18826  sylow2a  19695  islbs3  21290  toponsspwpw  23090  basdif0  23121  tgval  23123  eltg  23125  eltg2  23126  tgss  23136  basgen2  23157  2basgen  23158  bastop1  23161  topnex  23164  resttopon  23329  restabs  23333  restcld  23340  restfpw  23347  restcls  23349  restntr  23350  ordtbas2  23359  ordtbas  23360  lmfval  23400  cnrest  23453  cmpcov  23557  cmpsublem  23567  cmpsub  23568  2ndcomap  23626  islocfin  23685  txss12  23773  ptrescn  23807  trfbas2  24011  trfbas  24012  isfildlem  24025  snfbas  24034  trfil1  24054  trfil2  24055  trufil  24078  ssufl  24086  hauspwpwf1  24155  ustval  24371  metrest  24692  cnheibor  25125  metcld2  25477  bcthlem1  25494  mbfimaopn2  25827  0pledm  25843  dvbss  26071  dvreslem  26079  dvres2lem  26080  dvcnp2  26090  dvaddbr  26108  dvmulbr  26109  dvcnvrelem2  26188  elply2  26364  plyf  26366  plyss  26367  elplyr  26369  plyeq0lem  26378  plyeq0  26379  plyaddlem  26383  plymullem  26384  dgrlem  26397  coeidlem  26405  ulmcn  26573  pserulm  26596  rabexgfGS  32856  abrexdomjm  32864  aciunf1  33019  ress1r  33561  pcmplfin  34259  metidval  34289  sigagenss  34548  measval  34597  omsfval  34693  omssubaddlem  34698  omssubadd  34699  carsggect  34717  fineqvnttrclse  35545  erdsze2lem1  35703  erdsze2lem2  35704  cvxpconn  35742  elmsta  36048  dfon2lem3  36283  altxpexg  36478  ivthALT  36874  filnetlem3  36919  ttcexrg  37036  ttcsnexbig  37060  ttcexg  37071  bj-sselpwuni  37714  bj-elpwg  37716  bj-restsnss  37753  bj-restsnss2  37754  bj-restb  37764  bj-restuni2  37768  abrexdom  38409  sdclem2  38421  sdclem1  38422  brssr  39258  sticksstones4  42944  sticksstones14  42955  pssexg  43025  elrfirn  43454  pwssplit4  43844  hbtlem1  43878  hbtlem7  43880  inaex  45035  rabexgf  45772  dvnprodlem2  46689  qndenserrnbllem  47036  sge0ss  47154  psmeasurelem  47212  caragensplit  47242  omeunile  47247  caragenuncl  47255  omeunle  47258  omeiunlempt  47262  carageniuncllem2  47264  fcdmvafv2v  48001  prprval  48291  mpoexxg2  49146  gsumlsscl  49188  lincellss  49234  incat  50407