Theorem ssexg 5327

Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)

Assertion

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

Proof of Theorem ssexg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 4005	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 340	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3465	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5325	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3533	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  Vcvv 3461   ⊆ wss 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5303

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-in 3953  df-ss 3963

This theorem is referenced by:  ssexd  5328  prcssprc  5331  difexg  5333  rabexg  5337  elssabg  5342  elpw2g  5350  abssexg  5385  snexALT  5386  sess1  5649  sess2  5650  riinint  5974  resexg  6035  trsuc  6462  ordsssuc2  6466  mptexg  7237  mptexgf  7238  isofr2  7355  ofres  7708  brrpssg  7735  unexb  7755  xpexg  7757  abnexg  7763  difex2  7767  uniexr  7770  dmexg  7913  rnexg  7914  resiexg  7924  imaexg  7925  exse2  7929  cnvexg  7936  coexg  7941  fabexgOLD  7949  f1oabexgOLD  7953  resfunexgALT  7960  cofunexg  7961  fnexALT  7963  f1dmex  7969  oprabexd  7988  mpoexxg  8088  suppfnss  8202  tposexg  8254  tz7.48-3  8473  oaabs  8677  erex  8757  mapexOLD  8860  pmvalg  8865  elpmg  8871  elmapssres  8895  pmss12g  8897  ralxpmap  8924  ixpexg  8950  domssl  9028  ssdomg  9030  fiprc  9082  domunsncan  9109  infensuc  9192  pssnn  9205  ssfi  9210  pssnnOLD  9302  enp1i  9316  unbnn  9336  fodomfi  9365  fival  9451  fiss  9463  dffi3  9470  hartogslem2  9582  card2on  9593  wdomima2g  9625  unxpwdom2  9627  unxpwdom  9628  harwdom  9630  oemapvali  9723  ackbij1lem11  10269  cofsmo  10308  ssfin4  10349  fin23lem11  10356  ssfin2  10359  ssfin3ds  10369  isfin1-3  10425  hsmex3  10473  axdc2lem  10487  ac6num  10518  ttukeylem1  10548  dmct  10563  ondomon  10602  fpwwe2lem3  10672  fpwwe2lem11  10680  fpwwe2lem12  10681  canthwe  10690  wuncss  10784  genpv  11038  genpdm  11041  hashss  14421  hashf1lem1OLD  14469  wrdexb  14528  shftfval  15070  o1of2  15610  o1rlimmul  15616  isercolllem2  15665  isstruct2  17146  ressval3d  17255  ressval3dOLD  17256  ressabs  17258  prdsbas  17467  fnmrc  17615  mrcfval  17616  isacs1i  17665  mreacs  17666  isssc  17831  ipolerval  18552  ress0g  18750  sylow2a  19612  islbs3  21083  toponsspwpw  22907  basdif0  22939  tgval  22941  eltg  22943  eltg2  22944  tgss  22954  basgen2  22975  2basgen  22976  bastop1  22979  topnex  22982  resttopon  23148  restabs  23152  restcld  23159  restfpw  23166  restcls  23168  restntr  23169  ordtbas2  23178  ordtbas  23179  lmfval  23219  cnrest  23272  cmpcov  23376  cmpsublem  23386  cmpsub  23387  2ndcomap  23445  islocfin  23504  txss12  23592  ptrescn  23626  trfbas2  23830  trfbas  23831  isfildlem  23844  snfbas  23853  trfil1  23873  trfil2  23874  trufil  23897  ssufl  23905  hauspwpwf1  23974  ustval  24190  metrest  24516  cnheibor  24964  metcld2  25318  bcthlem1  25335  mbfimaopn2  25669  0pledm  25685  dvbss  25913  dvreslem  25921  dvres2lem  25922  dvcnp2  25932  dvcnp2OLD  25933  dvaddbr  25951  dvmulbr  25952  dvmulbrOLD  25953  dvcnvrelem2  26034  elply2  26215  plyf  26217  plyss  26218  elplyr  26220  plyeq0lem  26229  plyeq0  26230  plyaddlem  26234  plymullem  26235  dgrlem  26248  coeidlem  26256  ulmcn  26420  pserulm  26443  rabexgfGS  32418  abrexdomjm  32423  aciunf1  32571  ress1r  33076  pcmplfin  33631  metidval  33661  indval  33802  sigagenss  33938  measval  33987  omsfval  34084  omssubaddlem  34089  omssubadd  34090  carsggect  34108  erdsze2lem1  34983  erdsze2lem2  34984  cvxpconn  35022  elmsta  35328  dfon2lem3  35557  altxpexg  35750  ivthALT  35995  filnetlem3  36040  bj-sselpwuni  36705  bj-elpwg  36707  bj-restsnss  36738  bj-restsnss2  36739  bj-restb  36749  bj-restuni2  36753  abrexdom  37379  sdclem2  37391  sdclem1  37392  imaexALTV  37976  brssr  38147  sticksstones4  41795  sticksstones14  41806  pssexg  41891  elrfirn  42289  pwssplit4  42687  hbtlem1  42721  hbtlem7  42723  inaex  43908  rabexgf  44560  dvnprodlem1  45504  dvnprodlem2  45505  qndenserrnbllem  45852  sge0ss  45970  psmeasurelem  46028  caragensplit  46058  omeunile  46063  caragenuncl  46071  omeunle  46074  omeiunlempt  46078  carageniuncllem2  46080  fcdmvafv2v  46786  prprval  47023  mpoexxg2  47653  gsumlsscl  47699  lincellss  47746