Theorem trsbcVD 37337

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 36971 is trsbcVD 37337 without virtual deductions and was automatically derived from trsbcVD 37337.

1::	|- (. A e. B ->. A e. B ).
2:1:	|- (. A e. B ->. ( [. A / x ]. z e. y <-> z e. y ) ).
3:1:	|- (. A e. B ->. ( [. A / x ]. y e. x <-> y e. A ) ).
4:1:	|- (. A e. B ->. ( [. A / x ]. z e. x <-> z e. A ) ).
5:1,2,3,4:	|- (. A e. B ->. ( ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ).
6:1:	|- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) ) ).
7:5,6:	|- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ).
8::	|- ( ( z e. y -> ( y e. A -> z e. A ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) )
9:7,8:	|- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
10::	|- ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) )
11:10:	|- A. x ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) )
12:1,11:	|- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
13:9,12:	|- (. A e. B ->. ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
14:13:	|- (. A e. B ->. A. y ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
15:14:	|- (. A e. B ->. ( A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
16:1:	|- (. A e. B ->. ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
17:15,16:	|- (. A e. B ->. ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
18:17:	|- (. A e. B ->. A. z ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
19:18:	|- (. A e. B ->. ( A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
20:1:	|- (. A e. B ->. ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
21:19,20:	|- (. A e. B ->. ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
22::	|- ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
23:21,22:	|- (. A e. B ->. ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> Tr A ) ).
24::	|- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
25:24:	|- A. x ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
26:1,25:	|- (. A e. B ->. ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
27:23,26:	|- (. A e. B ->. ( [. A / x ]. Tr x <-> Tr A ) ).
qed:27:	|- ( A e. B -> ( [. A / x ]. Tr x <-> Tr A ) )

(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
trsbcVD	|- ( A e. B -> ( [. A / x ]. Tr x <-> Tr A ) )

Distinct variable group:   x, A

Allowed substitution hint:   B( x)

Proof of Theorem trsbcVD

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 37012	. . . . . . . . . . . . . 14 |- (. A e. B ->. A e. B ).
2		biidd 245	. . . . . . . . . . . . . . . 16 |- ( x = A -> ( z e. y <-> z e. y ) )
3	2	sbcieg 3288	. . . . . . . . . . . . . . 15 |- ( A e. B -> ( [. A / x ]. z e. y <-> z e. y ) )
4	1, 3	e1a 37074	. . . . . . . . . . . . . 14 |- (. A e. B ->. ( [. A / x ]. z e. y <-> z e. y ) ).
5		sbcel2gv 3315	. . . . . . . . . . . . . . 15 |- ( A e. B -> ( [. A / x ]. y e. x <-> y e. A ) )
6	1, 5	e1a 37074	. . . . . . . . . . . . . 14 |- (. A e. B ->. ( [. A / x ]. y e. x <-> y e. A ) ).
7		sbcel2gv 3315	. . . . . . . . . . . . . . 15 |- ( A e. B -> ( [. A / x ]. z e. x <-> z e. A ) )
8	1, 7	e1a 37074	. . . . . . . . . . . . . 14 |- (. A e. B ->. ( [. A / x ]. z e. x <-> z e. A ) ).
9		imbi13 36947	. . . . . . . . . . . . . . 15 |- ( ( [. A / x ]. z e. y <-> z e. y ) -> ( ( [. A / x ]. y e. x <-> y e. A ) -> ( ( [. A / x ]. z e. x <-> z e. A ) -> ( ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ) ) )
10	9	a1i 11	. . . . . . . . . . . . . 14 |- ( A e. B -> ( ( [. A / x ]. z e. y <-> z e. y ) -> ( ( [. A / x ]. y e. x <-> y e. A ) -> ( ( [. A / x ]. z e. x <-> z e. A ) -> ( ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ) ) ) )
11	1, 4, 6, 8, 10	e1111 37122	. . . . . . . . . . . . 13 |- (. A e. B ->. ( ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ).
12		sbcim2g 36969	. . . . . . . . . . . . . 14 |- ( A e. B -> ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) ) )
13	1, 12	e1a 37074	. . . . . . . . . . . . 13 |- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) ) ).
14		bibi1 334	. . . . . . . . . . . . . 14 |- ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) ) -> ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) <-> ( ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ) )
15	14	biimprcd 233	. . . . . . . . . . . . 13 |- ( ( ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) -> ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( [. A / x ]. z e. y -> ( [. A / x ]. y e. x -> [. A / x ]. z e. x ) ) ) -> ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ) )
16	11, 13, 15	e11 37135	. . . . . . . . . . . 12 |- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) ).
17		pm3.31 452	. . . . . . . . . . . . 13 |- ( ( z e. y -> ( y e. A -> z e. A ) ) -> ( ( z e. y /\ y e. A ) -> z e. A ) )
18		pm3.3 451	. . . . . . . . . . . . 13 |- ( ( ( z e. y /\ y e. A ) -> z e. A ) -> ( z e. y -> ( y e. A -> z e. A ) ) )
19	17, 18	impbii 192	. . . . . . . . . . . 12 |- ( ( z e. y -> ( y e. A -> z e. A ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) )
20		bibi1 334	. . . . . . . . . . . . 13 |- ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) -> ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) <-> ( ( z e. y -> ( y e. A -> z e. A ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
21	20	biimprd 231	. . . . . . . . . . . 12 |- ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( z e. y -> ( y e. A -> z e. A ) ) ) -> ( ( ( z e. y -> ( y e. A -> z e. A ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
22	16, 19, 21	e10 37141	. . . . . . . . . . 11 |- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
23		pm3.31 452	. . . . . . . . . . . . . 14 |- ( ( z e. y -> ( y e. x -> z e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
24		pm3.3 451	. . . . . . . . . . . . . 14 |- ( ( ( z e. y /\ y e. x ) -> z e. x ) -> ( z e. y -> ( y e. x -> z e. x ) ) )
25	23, 24	impbii 192	. . . . . . . . . . . . 13 |- ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) )
26	25	ax-gen 1677	. . . . . . . . . . . 12 |- A. x ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) )
27		sbcbi 36970	. . . . . . . . . . . 12 |- ( A e. B -> ( A. x ( ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) ) )
28	1, 26, 27	e10 37141	. . . . . . . . . . 11 |- (. A e. B ->. ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
29		bitr3 36937	. . . . . . . . . . . 12 |- ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
30	29	com12 31	. . . . . . . . . . 11 |- ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( ( [. A / x ]. ( z e. y -> ( y e. x -> z e. x ) ) <-> [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
31	22, 28, 30	e11 37135	. . . . . . . . . 10 |- (. A e. B ->. ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
32	31	gen11 37063	. . . . . . . . 9 |- (. A e. B ->. A. y ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
33		albi 1698	. . . . . . . . 9 |- ( A. y ( [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) )
34	32, 33	e1a 37074	. . . . . . . 8 |- (. A e. B ->. ( A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
35		sbcalgOLD 36973	. . . . . . . . 9 |- ( A e. B -> ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) )
36	1, 35	e1a 37074	. . . . . . . 8 |- (. A e. B ->. ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
37		bibi1 334	. . . . . . . . 9 |- ( ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) <-> ( A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
38	37	biimprcd 233	. . . . . . . 8 |- ( ( A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y [. A / x ]. ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
39	34, 36, 38	e11 37135	. . . . . . 7 |- (. A e. B ->. ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
40	39	gen11 37063	. . . . . 6 |- (. A e. B ->. A. z ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
41		albi 1698	. . . . . 6 |- ( A. z ( [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) )
42	40, 41	e1a 37074	. . . . 5 |- (. A e. B ->. ( A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
43		sbcalgOLD 36973	. . . . . 6 |- ( A e. B -> ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) )
44	1, 43	e1a 37074	. . . . 5 |- (. A e. B ->. ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
45		bibi1 334	. . . . . 6 |- ( ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) <-> ( A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
46	45	biimprcd 233	. . . . 5 |- ( ( A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z [. A / x ]. A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ) )
47	42, 44, 46	e11 37135	. . . 4 |- (. A e. B ->. ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ).
48		dftr2 4492	. . . 4 |- ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) )
49		biantr 945	. . . . 5 |- ( ( ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) /\ ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) ) -> ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> Tr A ) )
50	49	ex 441	. . . 4 |- ( ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( ( Tr A <-> A. z A. y ( ( z e. y /\ y e. A ) -> z e. A ) ) -> ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> Tr A ) ) )
51	47, 48, 50	e10 37141	. . 3 |- (. A e. B ->. ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> Tr A ) ).
52		dftr2 4492	. . . . 5 |- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
53	52	ax-gen 1677	. . . 4 |- A. x ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
54		sbcbi 36970	. . . 4 |- ( A e. B -> ( A. x ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) ) )
55	1, 53, 54	e10 37141	. . 3 |- (. A e. B ->. ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) ).
56		bibi1 334	. . . 4 |- ( ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( ( [. A / x ]. Tr x <-> Tr A ) <-> ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> Tr A ) ) )
57	56	biimprcd 233	. . 3 |- ( ( [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) <-> Tr A ) -> ( ( [. A / x ]. Tr x <-> [. A / x ]. A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) ) -> ( [. A / x ]. Tr x <-> Tr A ) ) )
58	51, 55, 57	e11 37135	. 2 |- (. A e. B ->. ( [. A / x ]. Tr x <-> Tr A ) ).
59	58	in1 37009	1 |- ( A e. B -> ( [. A / x ]. Tr x <-> Tr A ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   A.wal 1450   = wceq 1452   e. wcel 1904   [.wsbc 3255   Tr wtr 4490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-sbc 3256  df-in 3397  df-ss 3404  df-uni 4191  df-tr 4491  df-vd1 37008

This theorem is referenced by: (None)