Theorem ssexg 2721

Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized).

Assertion

Ref	Expression
ssexg	|- ((A (_ B /\ B e. C) -> A e. V)

Proof of Theorem ssexg

Step	Hyp	Ref	Expression
1		sseq2 2083	. . . 4 |- (x = B -> (A (_ x <-> A (_ B))
2	1	imbi1d 613	. . 3 |- (x = B -> ((A (_ x -> A e. V) <-> (A (_ B -> A e. V)))
3		visset 1813	. . . 4 |- x e. V
4	3	ssex 2719	. . 3 |- (A (_ x -> A e. V)
5	2, 4	vtoclg 1847	. 2 |- (B e. C -> (A (_ B -> A e. V))
6	5	impcom 351	1 |- ((A (_ B /\ B e. C) -> A e. V)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  Vcvv 1811   (_ wss 2047

This theorem is referenced by:  difexg 2722  rabexg 2724  elssabg 2726  elpw2g 2727  unexb 2873  difex2 2877  uniexb 2907  ordsssuc2 3059  xpexg 3259  dmexg 3358  rnexg 3359  resiexg 3396  imaexg 3416  cnvexg 3519  coexg 3524  resfunexg 3579  cofunexg 3580  fnex 3607  opabex2g 3611  fabexg 3653  f1oabexg 3700  f1dmex 3710  tz7.48-3 3958  oprabex2g 4020  oaabs 4252  mapex 4328  ixpexg 4358  ssdom2g 4409  pssnn 4534  cncfval 7264  istps3 7608  tgvalt 7616  eltgt 7618  eltg2t 7619  basgen2t 7639  iscld 7669  isnei 7718  blfval 7835  lmfval 7925  lmbr 7928  homeofval 10516  qusp 10555  fipfil2 10564  fipfil2OLD 10565  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  rcfpfil 10597  rcfpfilOLD 10598  sfvlim 10605

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053

Copyright terms: Public domain