Theorem tpss 2476

Description: A triplet of elements of a class is a subset of the class.

Hypotheses

Ref	Expression
tpss.1	|- A e. V
tpss.2	|- B e. V
tpss.3	|- C e. V

Assertion

Ref	Expression
tpss	|- ((A e. D /\ B e. D /\ C e. D) <-> {A, B, C} (_ D)

Proof of Theorem tpss

Step	Hyp	Ref	Expression
1		3jao 886	. . . . 5 |- (((x = A -> x e. D) /\ (x = B -> x e. D) /\ (x = C -> x e. D)) -> ((x = A \/ x = B \/ x = C) -> x e. D))
2		eleq1a 1543	. . . . 5 |- (A e. D -> (x = A -> x e. D))
3		eleq1a 1543	. . . . 5 |- (B e. D -> (x = B -> x e. D))
4		eleq1a 1543	. . . . 5 |- (C e. D -> (x = C -> x e. D))
5	1, 2, 3, 4	syl3an 868	. . . 4 |- ((A e. D /\ B e. D /\ C e. D) -> ((x = A \/ x = B \/ x = C) -> x e. D))
6		visset 1813	. . . . 5 |- x e. V
7	6	eltp 2439	. . . 4 |- (x e. {A, B, C} <-> (x = A \/ x = B \/ x = C))
8	5, 7	syl5ib 206	. . 3 |- ((A e. D /\ B e. D /\ C e. D) -> (x e. {A, B, C} -> x e. D))
9	8	ssrdv 2070	. 2 |- ((A e. D /\ B e. D /\ C e. D) -> {A, B, C} (_ D)
10		tpss.1	. . . . 5 |- A e. V
11	10	tpi1 2455	. . . 4 |- A e. {A, B, C}
12		ssel 2063	. . . 4 |- ({A, B, C} (_ D -> (A e. {A, B, C} -> A e. D))
13	11, 12	mpi 44	. . 3 |- ({A, B, C} (_ D -> A e. D)
14		tpss.2	. . . . 5 |- B e. V
15	14	tpi2 2456	. . . 4 |- B e. {A, B, C}
16		ssel 2063	. . . 4 |- ({A, B, C} (_ D -> (B e. {A, B, C} -> B e. D))
17	15, 16	mpi 44	. . 3 |- ({A, B, C} (_ D -> B e. D)
18		tpss.3	. . . . 5 |- C e. V
19	18	tpi3 2457	. . . 4 |- C e. {A, B, C}
20		ssel 2063	. . . 4 |- ({A, B, C} (_ D -> (C e. {A, B, C} -> C e. D))
21	19, 20	mpi 44	. . 3 |- ({A, B, C} (_ D -> C e. D)
22	13, 17, 21	3jca 819	. 2 |- ({A, B, C} (_ D -> (A e. D /\ B e. D /\ C e. D))
23	9, 22	impbi 157	1 |- ((A e. D /\ B e. D /\ C e. D) <-> {A, B, C} (_ D)

Syntax hints:   -> wi 3   <-> wb 146   \/ w3o 774   /\ w3a 775   = wceq 956   e. wcel 958  Vcvv 1811   (_ wss 2047  {ctp 2414

This theorem is referenced by:  fr3nr 2926

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-in 2051  df-ss 2053  df-sn 2412  df-pr 2413  df-tp 2415

Copyright terms: Public domain