Theorem ssexg 5293

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

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

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 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  ssexd  5294  prcssprc  5297  difexg  5299  elpw2g  5303  rabexgOLD  5308  elssabg  5313  abssexg  5352  snexALT  5353  sess1  5619  sess2  5620  riinint  5951  resexg  6014  trsuc  6441  ordsssuc2  6445  mptexg  7213  mptexgf  7214  isofr2  7337  ofres  7690  brrpssg  7719  unexb  7741  unexbOLD  7742  xpexg  7744  abnexg  7750  difex2  7754  uniexr  7757  dmexg  7897  rnexg  7898  resiexg  7908  imaexg  7909  exse2  7913  cnvexg  7920  coexg  7925  fabexgOLD  7935  f1oabexgOLD  7939  resfunexgALT  7946  cofunexg  7947  fnexALT  7949  f1dmex  7955  oprabexd  7974  mpoexxg  8074  suppfnss  8188  tposexg  8239  tz7.48-3  8458  oaabs  8660  erex  8743  mapexOLD  8846  pmvalg  8851  elpmg  8857  elmapssres  8881  pmss12g  8883  ralxpmap  8910  ixpexg  8936  domssl  9012  ssdomg  9014  fiprc  9059  domunsncan  9086  infensuc  9169  pssnn  9182  ssfi  9187  enp1i  9285  unbnn  9304  fodomfi  9322  fodomfiOLD  9342  fival  9424  fiss  9436  dffi3  9443  hartogslem2  9557  card2on  9568  wdomima2g  9600  unxpwdom2  9602  unxpwdom  9603  harwdom  9605  oemapvali  9698  ackbij1lem11  10243  cofsmo  10283  ssfin4  10324  fin23lem11  10331  ssfin2  10334  ssfin3ds  10344  isfin1-3  10400  hsmex3  10448  axdc2lem  10462  ac6num  10493  ttukeylem1  10523  dmct  10538  ondomon  10577  fpwwe2lem3  10647  fpwwe2lem11  10655  fpwwe2lem12  10656  canthwe  10665  wuncss  10759  genpv  11013  genpdm  11016  hashss  14427  wrdexb  14543  shftfval  15089  o1of2  15629  o1rlimmul  15635  isercolllem2  15682  isstruct2  17168  ressval3d  17267  ressabs  17269  prdsbas  17471  fnmrc  17619  mrcfval  17620  isacs1i  17669  mreacs  17670  isssc  17833  ipolerval  18542  ress0g  18740  sylow2a  19600  islbs3  21116  toponsspwpw  22860  basdif0  22891  tgval  22893  eltg  22895  eltg2  22896  tgss  22906  basgen2  22927  2basgen  22928  bastop1  22931  topnex  22934  resttopon  23099  restabs  23103  restcld  23110  restfpw  23117  restcls  23119  restntr  23120  ordtbas2  23129  ordtbas  23130  lmfval  23170  cnrest  23223  cmpcov  23327  cmpsublem  23337  cmpsub  23338  2ndcomap  23396  islocfin  23455  txss12  23543  ptrescn  23577  trfbas2  23781  trfbas  23782  isfildlem  23795  snfbas  23804  trfil1  23824  trfil2  23825  trufil  23848  ssufl  23856  hauspwpwf1  23925  ustval  24141  metrest  24463  cnheibor  24905  metcld2  25259  bcthlem1  25276  mbfimaopn2  25610  0pledm  25626  dvbss  25854  dvreslem  25862  dvres2lem  25863  dvcnp2  25873  dvcnp2OLD  25874  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvcnvrelem2  25975  elply2  26153  plyf  26155  plyss  26156  elplyr  26158  plyeq0lem  26167  plyeq0  26168  plyaddlem  26172  plymullem  26173  dgrlem  26186  coeidlem  26194  ulmcn  26360  pserulm  26383  rabexgfGS  32480  abrexdomjm  32488  aciunf1  32641  indval  32830  ress1r  33229  pcmplfin  33891  metidval  33921  sigagenss  34180  measval  34229  omsfval  34326  omssubaddlem  34331  omssubadd  34332  carsggect  34350  erdsze2lem1  35225  erdsze2lem2  35226  cvxpconn  35264  elmsta  35570  dfon2lem3  35803  altxpexg  35996  ivthALT  36353  filnetlem3  36398  bj-sselpwuni  37068  bj-elpwg  37070  bj-restsnss  37101  bj-restsnss2  37102  bj-restb  37112  bj-restuni2  37116  abrexdom  37754  sdclem2  37766  sdclem1  37767  imaexALTV  38348  brssr  38519  sticksstones4  42162  sticksstones14  42173  pssexg  42277  elrfirn  42718  pwssplit4  43113  hbtlem1  43147  hbtlem7  43149  inaex  44321  rabexgf  45048  dvnprodlem2  45976  qndenserrnbllem  46323  sge0ss  46441  psmeasurelem  46499  caragensplit  46529  omeunile  46534  caragenuncl  46542  omeunle  46545  omeiunlempt  46549  carageniuncllem2  46551  fcdmvafv2v  47265  prprval  47528  mpoexxg2  48313  gsumlsscl  48355  lincellss  48402  incat  49478