Theorem ssexg 5273

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  ssexd  5274  prcssprc  5277  difexg  5279  elpw2g  5283  rabexgOLD  5288  elssabg  5293  abssexg  5332  snexALT  5333  sess1  5596  sess2  5597  riinint  5924  resexg  5987  trsuc  6409  ordsssuc2  6413  mptexg  7177  mptexgf  7178  isofr2  7301  ofres  7652  brrpssg  7681  unexb  7703  unexbOLD  7704  xpexg  7706  abnexg  7712  difex2  7716  uniexr  7719  dmexg  7857  rnexg  7858  resiexg  7868  imaexg  7869  exse2  7873  cnvexg  7880  coexg  7885  fabexgOLD  7895  f1oabexgOLD  7899  resfunexgALT  7906  cofunexg  7907  fnexALT  7909  f1dmex  7915  oprabexd  7933  mpoexxg  8033  suppfnss  8145  tposexg  8196  tz7.48-3  8389  oaabs  8589  erex  8672  mapexOLD  8782  pmvalg  8787  elpmg  8793  elmapssres  8817  pmss12g  8819  ralxpmap  8846  ixpexg  8872  domssl  8946  ssdomg  8948  fiprc  8993  domunsncan  9018  infensuc  9096  pssnn  9109  ssfi  9114  enp1i  9200  unbnn  9219  fodomfi  9237  fodomfiOLD  9257  fival  9339  fiss  9351  dffi3  9358  hartogslem2  9472  card2on  9483  wdomima2g  9515  unxpwdom2  9517  unxpwdom  9518  harwdom  9520  oemapvali  9615  ackbij1lem11  10160  cofsmo  10200  ssfin4  10241  fin23lem11  10248  ssfin2  10251  ssfin3ds  10261  isfin1-3  10317  hsmex3  10365  axdc2lem  10379  ac6num  10410  ttukeylem1  10440  dmct  10455  ondomon  10494  fpwwe2lem3  10564  fpwwe2lem11  10572  fpwwe2lem12  10573  canthwe  10582  wuncss  10676  genpv  10930  genpdm  10933  hashss  14352  wrdexb  14468  shftfval  15013  o1of2  15556  o1rlimmul  15562  isercolllem2  15609  isstruct2  17096  ressval3d  17193  ressabs  17195  prdsbas  17397  fnmrc  17549  mrcfval  17550  isacs1i  17599  mreacs  17600  isssc  17763  ipolerval  18474  ress0g  18672  sylow2a  19534  islbs3  21098  toponsspwpw  22843  basdif0  22874  tgval  22876  eltg  22878  eltg2  22879  tgss  22889  basgen2  22910  2basgen  22911  bastop1  22914  topnex  22917  resttopon  23082  restabs  23086  restcld  23093  restfpw  23100  restcls  23102  restntr  23103  ordtbas2  23112  ordtbas  23113  lmfval  23153  cnrest  23206  cmpcov  23310  cmpsublem  23320  cmpsub  23321  2ndcomap  23379  islocfin  23438  txss12  23526  ptrescn  23560  trfbas2  23764  trfbas  23765  isfildlem  23778  snfbas  23787  trfil1  23807  trfil2  23808  trufil  23831  ssufl  23839  hauspwpwf1  23908  ustval  24124  metrest  24446  cnheibor  24888  metcld2  25241  bcthlem1  25258  mbfimaopn2  25592  0pledm  25608  dvbss  25836  dvreslem  25844  dvres2lem  25845  dvcnp2  25855  dvcnp2OLD  25856  dvaddbr  25874  dvmulbr  25875  dvmulbrOLD  25876  dvcnvrelem2  25957  elply2  26135  plyf  26137  plyss  26138  elplyr  26140  plyeq0lem  26149  plyeq0  26150  plyaddlem  26154  plymullem  26155  dgrlem  26168  coeidlem  26176  ulmcn  26342  pserulm  26365  rabexgfGS  32479  abrexdomjm  32487  aciunf1  32638  indval  32827  ress1r  33202  pcmplfin  33844  metidval  33874  sigagenss  34133  measval  34182  omsfval  34279  omssubaddlem  34284  omssubadd  34285  carsggect  34303  erdsze2lem1  35184  erdsze2lem2  35185  cvxpconn  35223  elmsta  35529  dfon2lem3  35767  altxpexg  35960  ivthALT  36317  filnetlem3  36362  bj-sselpwuni  37032  bj-elpwg  37034  bj-restsnss  37065  bj-restsnss2  37066  bj-restb  37076  bj-restuni2  37080  abrexdom  37718  sdclem2  37730  sdclem1  37731  brssr  38486  sticksstones4  42131  sticksstones14  42142  pssexg  42208  elrfirn  42677  pwssplit4  43072  hbtlem1  43106  hbtlem7  43108  inaex  44280  rabexgf  45012  dvnprodlem2  45939  qndenserrnbllem  46286  sge0ss  46404  psmeasurelem  46462  caragensplit  46492  omeunile  46497  caragenuncl  46505  omeunle  46508  omeiunlempt  46512  carageniuncllem2  46514  fcdmvafv2v  47231  prprval  47509  mpoexxg2  48320  gsumlsscl  48362  lincellss  48409  incat  49584