Theorem ssexg 5285

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 4097	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
2		inex2g 5284	. . 3 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ∩ 𝐵) ∈ V)
3		eleq1 2852	. . . 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 2147  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  ssex  5286  ssexd  5290  prcssprc  5293  difexg  5295  elpw2g  5299  elssabg  5308  abssexg  5348  snexALT  5349  sess1  5620  sess2  5621  riinint  5960  resexg  6027  trsuc  6467  ordsssuc2  6471  mptexg  7247  mptexgf  7248  isofr2  7372  ofres  7733  brrpssg  7762  unexb  7784  xpexg  7785  abnexg  7791  difex2  7795  uniexr  7798  dmexg  7934  rnexg  7935  resiexg  7945  imaexg  7946  exse2  7950  cnvexg  7957  coexg  7962  resfunexgALT  7981  cofunexg  7982  fnexALT  7984  f1dmex  7990  oprabexd  8008  mpoexxg  8110  suppfnss  8231  tposexg  8282  tz7.48-3  8479  oaabs  8682  erex  8767  pmvalg  8882  elpmg  8888  elmapssres  8919  pmss12g  8922  ralxpmap  8949  ixpexg  8975  domssl  9050  ssdomg  9052  fiprc  9097  domunsncan  9121  infensuc  9199  pssnn  9209  ssfi  9213  enp1i  9295  unbnn  9313  fodomfi  9329  fival  9428  fiss  9440  dffi3  9447  hartogslem2  9561  card2on  9572  wdomima2g  9604  unxpwdom2  9606  unxpwdom  9607  harwdom  9609  oemapvali  9709  ackbij1lem11  10331  cofsmo  10371  ssfin4  10412  fin23lem11  10419  ssfin2  10422  ssfin3ds  10432  isfin1-3  10488  hsmex3  10536  axdc2lem  10550  ac6num  10581  ac6  10582  ttukeylem1  10611  dmctOLD  10627  fpwwe2lem3  10742  fpwwe2lem11  10750  fpwwe2lem12  10751  canthwe  10760  wuncss  10854  genpv  11108  genpdm  11111  indval  12347  hashss  14577  wrdexb  14694  shftfval  15249  o1of2  15806  o1rlimmul  15812  isercolllem2  15859  isstruct2  17353  ressval3d  17450  ressabs  17452  prdsbas  17654  fnmrc  17807  mrcfval  17808  isacs1i  17857  mreacs  17858  isssc  18021  ipolerval  18732  chnexg  18818  ress0gOLD  18981  sylow2a  19860  islbs3  21460  toponsspwpw  23267  basdif0  23298  tgval  23300  eltg  23302  eltg2  23303  tgss  23313  basgen2  23334  2basgen  23335  bastop1  23338  topnex  23341  resttopon  23506  restabs  23510  restcld  23517  restfpw  23524  restcls  23526  restntr  23527  ordtbas2  23536  ordtbas  23537  lmfval  23577  cnrest  23630  cmpcov  23734  cmpsublem  23744  cmpsub  23745  2ndcomap  23804  islocfin  23863  txss12  23951  ptrescn  23985  trfbas2  24189  trfbas  24190  isfildlem  24203  snfbas  24212  trfil1  24232  trfil2  24233  trufil  24256  ssufl  24264  hauspwpwf1  24333  ustval  24549  metrest  24870  cnheibor  25303  metcld2  25655  bcthlem1  25672  mbfimaopn2  26005  0pledm  26021  dvbss  26248  dvreslem  26256  dvres2lem  26257  dvcnp2  26267  dvaddbr  26285  dvmulbr  26286  dvcnvrelem2  26365  elply2  26541  plyf  26543  plyss  26544  elplyr  26546  plyeq0lem  26556  plyeq0  26557  plyaddlem  26561  plymullem  26562  dgrlem  26575  coeidlem  26583  ulmcn  26753  pserulm  26776  rabexgfGS  33164  abrexdomjm  33172  aciunf1  33326  ress1r  33860  pcmplfin  34559  metidval  34589  sigagenss  34849  measval  34898  omsfval  34993  omssubaddlem  34998  carsggect  35017  abweex  35798  acwer1prc  35851  fineqvnttrclse  35891  erdsze2lem1  36134  erdsze2lem2  36135  cvxpconn  36173  elmsta  36479  dfon2lem3  36724  altxpexg  36920  ivthALT  37300  filnetlem3  37345  ttcexrg  37462  ttcsnexbig  37486  ttcexg  37497  bj-sselpwuni  38155  bj-elpwg  38157  bj-restsnss  38194  bj-restsnss2  38195  bj-restb  38205  bj-restuni2  38209  abrexdom  38855  sdclem2  38867  sdclem1  38868  brssr  39704  sticksstones4  43390  sticksstones14  43401  pssexg  43471  elrfirn  43897  pwssplit4  44282  hbtlem1  44315  hbtlem7  44317  inaex  45471  rabexgf  46244  dvnprodlem2  47160  qndenserrnbllem  47507  sge0ss  47625  psmeasurelem  47683  caragensplit  47713  omeunile  47718  caragenuncl  47726  omeunle  47729  omeiunlempt  47733  carageniuncllem2  47735  fcdmvafv2v  48509  prprval  48799  mpoexxg2  49653  gsumlsscl  49695  lincellss  49741  incat  50942