Theorem onfrALTlem5VD 31626

Description: Virtual deduction proof of onfrALTlem5 31255. 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. onfrALTlem5 31255 is onfrALTlem5VD 31626 without virtual deductions and was automatically derived from onfrALTlem5VD 31626.

1::	|- a e. _V
2:1:	|- ( a i^i x ) e. _V
3:2:	|- ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) )
4:3:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> -. ( a i^i x ) = (/) )
5::	|- ( ( a i^i x ) =/= (/) <-> -. ( a i^i x ) = (/) )
6:4,5:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) =/= (/) )
7:2:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
8::	|- ( b =/= (/) <-> -. b = (/) )
9:8:	|- A. b ( b =/= (/) <-> -. b = (/) )
10:2,9:	|- ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
11:7,10:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. b =/= (/) )
12:6,11:	|- ( [. ( a i^i x ) / b ]. b =/= (/) <-> ( a i^i x ) =/= (/) )
13:2:	|- ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) )
14:12,13:	|- ( ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
15:2:	|- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) )
16:15,14:	|- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
17:2:	|- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y )
18:2:	|- [_ ( a i^i x ) / b ]_ b = ( a i^i x )
19:2:	|- [_ ( a i^i x ) / b ]_ y = y
20:18,19:	|- ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) = ( ( a i^i x ) i^i y )
21:17,20:	|- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( ( a i^i x ) i^i y )
22:2:	|- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) )
23:2:	|- [_ ( a i^i x ) / b ]_ (/) = (/)
24:21,23:	|- ( [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) <-> ( ( a i^i x ) i^i y ) = (/) )
25:22,24:	|- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> ( ( a i^i x ) i^i y ) = (/) )
26:2:	|- ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) )
27:25,26:	|- ( ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
28:2:	|- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) )
29:27,28:	|- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
30:29:	|- A. y ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
31:30:	|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
32::	|- ( E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
33:31,32:	|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
34:2:	|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
35:33,34:	|- ( [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
36::	|- ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
37:36:	|- A. b ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
38:2,37:	|- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
39:35,38:	|- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
40:16,39:	|- ( ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
41:2:	|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) )
qed:40,41:	|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )

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

Assertion

Ref	Expression
onfrALTlem5VD	|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )

Distinct variable groups:   a, b, y   x, b, y

Proof of Theorem onfrALTlem5VD

Step	Hyp	Ref	Expression
1		vex 2980	. . . 4 |- a e. _V
2	1	inex1 4438	. . 3 |- ( a i^i x ) e. _V
3		sbcimg 3233	. . 3 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) ) )
4	2, 3	e0a 31510	. 2 |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) )
5		sbcangOLD 3235	. . . . 5 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) ) )
6	2, 5	e0a 31510	. . . 4 |- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) )
7		sseq1 3382	. . . . . . 7 |- ( b = ( a i^i x ) -> ( b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) ) )
8	7	sbcieg 3224	. . . . . 6 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) ) )
9	2, 8	e0a 31510	. . . . 5 |- ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) )
10		sbcng 3232	. . . . . . . . 9 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. -. b = (/) <-> -. [. ( a i^i x ) / b ]. b = (/) ) )
11	10	bicomd 201	. . . . . . . 8 |- ( ( a i^i x ) e. _V -> ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) ) )
12	2, 11	e0a 31510	. . . . . . 7 |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
13		df-ne 2613	. . . . . . . . 9 |- ( b =/= (/) <-> -. b = (/) )
14	13	ax-gen 1591	. . . . . . . 8 |- A. b ( b =/= (/) <-> -. b = (/) )
15		sbcbi 31251	. . . . . . . 8 |- ( ( a i^i x ) e. _V -> ( A. b ( b =/= (/) <-> -. b = (/) ) -> ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) ) ) )
16	2, 14, 15	e00 31506	. . . . . . 7 |- ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
17	12, 16	bitr4i 252	. . . . . 6 |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. b =/= (/) )
18		eqsbc3 3231	. . . . . . . . 9 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) ) )
19	2, 18	e0a 31510	. . . . . . . 8 |- ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) )
20	19	notbii 296	. . . . . . 7 |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> -. ( a i^i x ) = (/) )
21		df-ne 2613	. . . . . . 7 |- ( ( a i^i x ) =/= (/) <-> -. ( a i^i x ) = (/) )
22	20, 21	bitr4i 252	. . . . . 6 |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) =/= (/) )
23	17, 22	bitr3i 251	. . . . 5 |- ( [. ( a i^i x ) / b ]. b =/= (/) <-> ( a i^i x ) =/= (/) )
24	9, 23	anbi12i 697	. . . 4 |- ( ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
25	6, 24	bitri 249	. . 3 |- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
26		df-rex 2726	. . . . . 6 |- ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
27	26	ax-gen 1591	. . . . 5 |- A. b ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
28		sbcbi 31251	. . . . 5 |- ( ( a i^i x ) e. _V -> ( A. b ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) ) -> ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) ) ) )
29	2, 27, 28	e00 31506	. . . 4 |- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
30		sbcexgOLD 3246	. . . . . . 7 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) ) )
31	30	bicomd 201	. . . . . 6 |- ( ( a i^i x ) e. _V -> ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) ) )
32	2, 31	e0a 31510	. . . . 5 |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
33		sbcangOLD 3235	. . . . . . . . . 10 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) ) )
34	2, 33	e0a 31510	. . . . . . . . 9 |- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) )
35		sbcel2gv 3258	. . . . . . . . . . 11 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) ) )
36	2, 35	e0a 31510	. . . . . . . . . 10 |- ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) )
37		sbceqg 3682	. . . . . . . . . . . 12 |- ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) ) )
38	2, 37	e0a 31510	. . . . . . . . . . 11 |- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) )
39		csbingOLD 3718	. . . . . . . . . . . . . 14 |- ( ( a i^i x ) e. _V -> [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) )
40	2, 39	e0a 31510	. . . . . . . . . . . . 13 |- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y )
41		csbvarg 3705	. . . . . . . . . . . . . . 15 |- ( ( a i^i x ) e. _V -> [_ ( a i^i x ) / b ]_ b = ( a i^i x ) )
42	2, 41	e0a 31510	. . . . . . . . . . . . . 14 |- [_ ( a i^i x ) / b ]_ b = ( a i^i x )
43		csbconstg 3306	. . . . . . . . . . . . . . 15 |- ( ( a i^i x ) e. _V -> [_ ( a i^i x ) / b ]_ y = y )
44	2, 43	e0a 31510	. . . . . . . . . . . . . 14 |- [_ ( a i^i x ) / b ]_ y = y
45	42, 44	ineq12i 3555	. . . . . . . . . . . . 13 |- ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) = ( ( a i^i x ) i^i y )
46	40, 45	eqtri 2463	. . . . . . . . . . . 12 |- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( ( a i^i x ) i^i y )
47		csbconstg 3306	. . . . . . . . . . . . 13 |- ( ( a i^i x ) e. _V -> [_ ( a i^i x ) / b ]_ (/) = (/) )
48	2, 47	e0a 31510	. . . . . . . . . . . 12 |- [_ ( a i^i x ) / b ]_ (/) = (/)
49	46, 48	eqeq12i 2456	. . . . . . . . . . 11 |- ( [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) <-> ( ( a i^i x ) i^i y ) = (/) )
50	38, 49	bitri 249	. . . . . . . . . 10 |- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> ( ( a i^i x ) i^i y ) = (/) )
51	36, 50	anbi12i 697	. . . . . . . . 9 |- ( ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
52	34, 51	bitri 249	. . . . . . . 8 |- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
53	52	ax-gen 1591	. . . . . . 7 |- A. y ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
54		exbi 1633	. . . . . . 7 |- ( A. y ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) -> ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ) )
55	53, 54	e0a 31510	. . . . . 6 |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
56		df-rex 2726	. . . . . 6 |- ( E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
57	55, 56	bitr4i 252	. . . . 5 |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
58	32, 57	bitr3i 251	. . . 4 |- ( [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
59	29, 58	bitri 249	. . 3 |- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
60	25, 59	imbi12i 326	. 2 |- ( ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
61	4, 60	bitri 249	1 |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1367   = wceq 1369   E.wex 1586   e. wcel 1756   =/= wne 2611   E.wrex 2721   _Vcvv 2977   [.wsbc 3191   [_csb 3293   i^i cin 3332   C_ wss 3333   (/)c0 3642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-in 3340  df-ss 3347

This theorem is referenced by: (None)