Theorem ssexg 5323

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 4010	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 341	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3484	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5321	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3554	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 407	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  ssexd  5324  prcssprc  5327  difexg  5329  elpw2g  5333  rabexgOLD  5338  elssabg  5343  abssexg  5382  snexALT  5383  sess1  5650  sess2  5651  riinint  5982  resexg  6045  trsuc  6471  ordsssuc2  6475  mptexg  7241  mptexgf  7242  isofr2  7364  ofres  7716  brrpssg  7745  unexb  7767  unexbOLD  7768  xpexg  7770  abnexg  7776  difex2  7780  uniexr  7783  dmexg  7923  rnexg  7924  resiexg  7934  imaexg  7935  exse2  7939  cnvexg  7946  coexg  7951  fabexgOLD  7961  f1oabexgOLD  7965  resfunexgALT  7972  cofunexg  7973  fnexALT  7975  f1dmex  7981  oprabexd  8000  mpoexxg  8100  suppfnss  8214  tposexg  8265  tz7.48-3  8484  oaabs  8686  erex  8769  mapexOLD  8872  pmvalg  8877  elpmg  8883  elmapssres  8907  pmss12g  8909  ralxpmap  8936  ixpexg  8962  domssl  9038  ssdomg  9040  fiprc  9085  domunsncan  9112  infensuc  9195  pssnn  9208  ssfi  9213  enp1i  9313  unbnn  9332  fodomfi  9350  fodomfiOLD  9370  fival  9452  fiss  9464  dffi3  9471  hartogslem2  9583  card2on  9594  wdomima2g  9626  unxpwdom2  9628  unxpwdom  9629  harwdom  9631  oemapvali  9724  ackbij1lem11  10269  cofsmo  10309  ssfin4  10350  fin23lem11  10357  ssfin2  10360  ssfin3ds  10370  isfin1-3  10426  hsmex3  10474  axdc2lem  10488  ac6num  10519  ttukeylem1  10549  dmct  10564  ondomon  10603  fpwwe2lem3  10673  fpwwe2lem11  10681  fpwwe2lem12  10682  canthwe  10691  wuncss  10785  genpv  11039  genpdm  11042  hashss  14448  wrdexb  14563  shftfval  15109  o1of2  15649  o1rlimmul  15655  isercolllem2  15702  isstruct2  17186  ressval3d  17292  ressabs  17294  prdsbas  17502  fnmrc  17650  mrcfval  17651  isacs1i  17700  mreacs  17701  isssc  17864  ipolerval  18577  ress0g  18775  sylow2a  19637  islbs3  21157  toponsspwpw  22928  basdif0  22960  tgval  22962  eltg  22964  eltg2  22965  tgss  22975  basgen2  22996  2basgen  22997  bastop1  23000  topnex  23003  resttopon  23169  restabs  23173  restcld  23180  restfpw  23187  restcls  23189  restntr  23190  ordtbas2  23199  ordtbas  23200  lmfval  23240  cnrest  23293  cmpcov  23397  cmpsublem  23407  cmpsub  23408  2ndcomap  23466  islocfin  23525  txss12  23613  ptrescn  23647  trfbas2  23851  trfbas  23852  isfildlem  23865  snfbas  23874  trfil1  23894  trfil2  23895  trufil  23918  ssufl  23926  hauspwpwf1  23995  ustval  24211  metrest  24537  cnheibor  24987  metcld2  25341  bcthlem1  25358  mbfimaopn2  25692  0pledm  25708  dvbss  25936  dvreslem  25944  dvres2lem  25945  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcnvrelem2  26057  elply2  26235  plyf  26237  plyss  26238  elplyr  26240  plyeq0lem  26249  plyeq0  26250  plyaddlem  26254  plymullem  26255  dgrlem  26268  coeidlem  26276  ulmcn  26442  pserulm  26465  rabexgfGS  32518  abrexdomjm  32526  aciunf1  32673  indval  32838  ress1r  33238  pcmplfin  33859  metidval  33889  sigagenss  34150  measval  34199  omsfval  34296  omssubaddlem  34301  omssubadd  34302  carsggect  34320  erdsze2lem1  35208  erdsze2lem2  35209  cvxpconn  35247  elmsta  35553  dfon2lem3  35786  altxpexg  35979  ivthALT  36336  filnetlem3  36381  bj-sselpwuni  37051  bj-elpwg  37053  bj-restsnss  37084  bj-restsnss2  37085  bj-restb  37095  bj-restuni2  37099  abrexdom  37737  sdclem2  37749  sdclem1  37750  imaexALTV  38331  brssr  38502  sticksstones4  42150  sticksstones14  42161  pssexg  42265  elrfirn  42706  pwssplit4  43101  hbtlem1  43135  hbtlem7  43137  inaex  44316  rabexgf  45029  dvnprodlem2  45962  qndenserrnbllem  46309  sge0ss  46427  psmeasurelem  46485  caragensplit  46515  omeunile  46520  caragenuncl  46528  omeunle  46531  omeiunlempt  46535  carageniuncllem2  46537  fcdmvafv2v  47248  prprval  47501  mpoexxg2  48254  gsumlsscl  48296  lincellss  48343