Theorem ssexg 5247

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 3947	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 342	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 3436	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 5245	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 3505	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 408	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  ssexd  5248  prcssprc  5249  difexg  5251  rabexg  5255  elssabg  5260  elpw2g  5268  abssexg  5305  snexALT  5306  sess1  5557  sess2  5558  riinint  5877  resexg  5937  trsuc  6350  ordsssuc2  6354  mptexg  7097  mptexgf  7098  isofr2  7215  ofres  7552  brrpssg  7578  unexb  7598  xpexg  7600  abnexg  7606  difex2  7610  uniexr  7613  dmexg  7750  rnexg  7751  resiexg  7761  imaexg  7762  exse2  7764  cnvexg  7771  coexg  7776  fabexg  7781  f1oabexg  7783  resfunexgALT  7790  cofunexg  7791  fnexALT  7793  f1dmex  7799  oprabexd  7818  mpoexxg  7916  suppfnss  8005  tposexg  8056  tz7.48-3  8275  oaabs  8478  erex  8522  mapex  8621  pmvalg  8626  elpmg  8631  elmapssres  8655  pmss12g  8657  ralxpmap  8684  ixpexg  8710  ssdomg  8786  fiprc  8835  domunsncan  8859  infensuc  8942  pssnn  8951  ssfi  8956  pssnnOLD  9040  unbnn  9070  fodomfi  9092  fival  9171  fiss  9183  dffi3  9190  hartogslem2  9302  card2on  9313  wdomima2g  9345  unxpwdom2  9347  unxpwdom  9348  harwdom  9350  oemapvali  9442  ackbij1lem11  9986  cofsmo  10025  ssfin4  10066  fin23lem11  10073  ssfin2  10076  ssfin3ds  10086  isfin1-3  10142  hsmex3  10190  axdc2lem  10204  ac6num  10235  ttukeylem1  10265  dmct  10280  ondomon  10319  fpwwe2lem3  10389  fpwwe2lem11  10397  fpwwe2lem12  10398  canthwe  10407  wuncss  10501  genpv  10755  genpdm  10758  hashss  14124  hashf1lem1OLD  14169  wrdexb  14228  shftfval  14781  o1of2  15322  o1rlimmul  15328  isercolllem2  15377  isstruct2  16850  ressval3d  16956  ressval3dOLD  16957  ressabs  16959  prdsbas  17168  fnmrc  17316  mrcfval  17317  isacs1i  17366  mreacs  17367  isssc  17532  ipolerval  18250  ress0g  18413  sylow2a  19224  islbs3  20417  toponsspwpw  22071  basdif0  22103  tgval  22105  eltg  22107  eltg2  22108  tgss  22118  basgen2  22139  2basgen  22140  bastop1  22143  topnex  22146  resttopon  22312  restabs  22316  restcld  22323  restfpw  22330  restcls  22332  restntr  22333  ordtbas2  22342  ordtbas  22343  lmfval  22383  cnrest  22436  cmpcov  22540  cmpsublem  22550  cmpsub  22551  2ndcomap  22609  islocfin  22668  txss12  22756  ptrescn  22790  trfbas2  22994  trfbas  22995  isfildlem  23008  snfbas  23017  trfil1  23037  trfil2  23038  trufil  23061  ssufl  23069  hauspwpwf1  23138  ustval  23354  metrest  23680  cnheibor  24118  metcld2  24471  bcthlem1  24488  mbfimaopn2  24821  0pledm  24837  dvbss  25065  dvreslem  25073  dvres2lem  25074  dvcnp2  25084  dvaddbr  25102  dvmulbr  25103  dvcnvrelem2  25182  elply2  25357  plyf  25359  plyss  25360  elplyr  25362  plyeq0lem  25371  plyeq0  25372  plyaddlem  25376  plymullem  25377  dgrlem  25390  coeidlem  25398  ulmcn  25558  pserulm  25581  rabexgfGS  30846  abrexdomjm  30852  aciunf1  31000  ress1r  31486  pcmplfin  31810  metidval  31840  indval  31981  sigagenss  32117  measval  32166  omsfval  32261  omssubaddlem  32266  omssubadd  32267  carsggect  32285  erdsze2lem1  33165  erdsze2lem2  33166  cvxpconn  33204  elmsta  33510  dfon2lem3  33761  altxpexg  34280  ivthALT  34524  filnetlem3  34569  bj-sselpwuni  35223  bj-elpwg  35225  bj-restsnss  35254  bj-restsnss2  35255  bj-restb  35265  bj-restuni2  35269  abrexdom  35888  sdclem2  35900  sdclem1  35901  imaexALTV  36465  brssr  36619  sticksstones4  40105  sticksstones14  40116  pssexg  40201  elrfirn  40517  pwssplit4  40914  hbtlem1  40948  hbtlem7  40950  inaex  41915  rabexgf  42567  dvnprodlem1  43487  dvnprodlem2  43488  qndenserrnbllem  43835  sge0ss  43950  psmeasurelem  44008  caragensplit  44038  omeunile  44043  caragenuncl  44051  omeunle  44054  omeiunlempt  44058  carageniuncllem2  44060  frnvafv2v  44728  prprval  44966  mpoexxg2  45673  gsumlsscl  45719  lincellss  45767