Theorem eceqoveq 7435

Description: Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)

Hypotheses

Ref	Expression
eceqoveq.5
eceqoveq.7
eceqoveq.8
eceqoveq.9
eceqoveq.10

Assertion

Ref	Expression
eceqoveq

Distinct variable groups:   ,,   ,S,   ,,   ,,   ,,   ,,

Proof of Theorem eceqoveq

Step	Hyp	Ref	Expression
1		opelxpi 5036	. . . . . . . 8
2	1	ad2antrr 725	. . . . . . 7
3		eceqoveq.5	. . . . . . . . 9
4	3	a1i 11	. . . . . . . 8
5		simpr 461	. . . . . . . 8
6	4, 5	ereldm 7374	. . . . . . 7
7	2, 6	mpbid 210	. . . . . 6
8		opelxp2 5038	. . . . . 6
9	7, 8	syl 16	. . . . 5
10	9	ex 434	. . . 4
11		eceqoveq.9	. . . . . . . 8
12	11	caovcl 6469	. . . . . . 7
13		eleq1 2529	. . . . . . 7
14	12, 13	syl5ibr 221	. . . . . 6
15		eceqoveq.7	. . . . . . . 8
16		eceqoveq.8	. . . . . . . 8
17	15, 16	ndmovrcl 6461	. . . . . . 7
18	17	simprd 463	. . . . . 6
19	14, 18	syl6com 35	. . . . 5
20	19	adantll 713	. . . 4
21	3	a1i 11	. . . . . . 7
22	1	adantr 465	. . . . . . 7
23	21, 22	erth 7375	. . . . . 6
24		eceqoveq.10	. . . . . 6
25	23, 24	bitr3d 255	. . . . 5
26	25	expr 615	. . . 4
27	10, 20, 26	pm5.21ndd 354	. . 3
28	27	an32s 804	. 2
29		eqcom 2466	. . . 4
30		erdm 7340	. . . . . . . . . . . 12
31	3, 30	ax-mp 5	. . . . . . . . . . 11
32	31	eleq2i 2535	. . . . . . . . . 10
33		ecdmn0 7373	. . . . . . . . . 10
34		opelxp 5034	. . . . . . . . . 10
35	32, 33, 34	3bitr3i 275	. . . . . . . . 9
36	35	simplbi2 625	. . . . . . . 8
37	36	ad2antlr 726	. . . . . . 7
38	37	necon2bd 2672	. . . . . 6
39		simpr 461	. . . . . . . 8
40	39	con3i 135	. . . . . . 7
41	15	ndmov 6459	. . . . . . 7
42	40, 41	syl 16	. . . . . 6
43	38, 42	syl6 33	. . . . 5
44		eleq1 2529	. . . . . . 7
45	16, 44	mtbiri 303	. . . . . 6
46	35	simprbi 464	. . . . . . . 8
47	11	caovcl 6469	. . . . . . . . . 10
48	47	ex 434	. . . . . . . . 9
49	48	ad2antrr 725	. . . . . . . 8
50	46, 49	syl5 32	. . . . . . 7
51	50	necon1bd 2675	. . . . . 6
52	45, 51	syl5 32	. . . . 5
53	43, 52	impbid 191	. . . 4
54	29, 53	syl5bb 257	. . 3
55	31	eleq2i 2535	. . . . . . . 8
56		ecdmn0 7373	. . . . . . . 8
57		opelxp 5034	. . . . . . . 8
58	55, 56, 57	3bitr3i 275	. . . . . . 7
59	58	simprbi 464	. . . . . 6
60	59	necon1bi 2690	. . . . 5
61	60	adantl 466	. . . 4
62	61	eqeq1d 2459	. . 3
63		simpl 457	. . . . . . 7
64	63	con3i 135	. . . . . 6
65	15	ndmov 6459	. . . . . 6
66	64, 65	syl 16	. . . . 5
67	66	adantl 466	. . . 4
68	67	eqeq2d 2471	. . 3
69	54, 62, 68	3bitr4d 285	. 2
70	28, 69	pm2.61dan 791	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652  c0 3784  <.cop 4035   class class class wbr 4452  X.cxp 5002  domcdm 5004  (class class class)co 6296  Erwer 7327  [cec 7328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fv 5601  df-ov 6299  df-er 7330  df-ec 7332