Theorem nn0opth2t 4726

Description: An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opth 4724.

Assertion

Ref	Expression
nn0opth2t	|- (((A e. NN0 /\ B e. NN0) /\ (C e. NN0 /\ D e. NN0)) -> ((((A + B)^2) + B) = (((C + D)^2) + D) <-> (A = C /\ B = D)))

Proof of Theorem nn0opth2t

Step	Hyp	Ref	Expression
1		opreq1 3006	. . . . . 6 |- (A = if(A e. NN0, A, 0) -> (A + B) = (if(A e. NN0, A, 0) + B))
2	1	opreq1d 3012	. . . . 5 |- (A = if(A e. NN0, A, 0) -> ((A + B)^2) = ((if(A e. NN0, A, 0) + B)^2))
3	2	opreq1d 3012	. . . 4 |- (A = if(A e. NN0, A, 0) -> (((A + B)^2) + B) = (((if(A e. NN0, A, 0) + B)^2) + B))
4	3	cleq1d 1109	. . 3 |- (A = if(A e. NN0, A, 0) -> ((((A + B)^2) + B) = (((C + D)^2) + D) <-> (((if(A e. NN0, A, 0) + B)^2) + B) = (((C + D)^2) + D)))
5		cleq1 1107	. . . 4 |- (A = if(A e. NN0, A, 0) -> (A = C <-> if(A e. NN0, A, 0) = C))
6	5	anbi1d 469	. . 3 |- (A = if(A e. NN0, A, 0) -> ((A = C /\ B = D) <-> (if(A e. NN0, A, 0) = C /\ B = D)))
7	4, 6	bibi12d 477	. 2 |- (A = if(A e. NN0, A, 0) -> (((((A + B)^2) + B) = (((C + D)^2) + D) <-> (A = C /\ B = D)) <-> ((((if(A e. NN0, A, 0) + B)^2) + B) = (((C + D)^2) + D) <-> (if(A e. NN0, A, 0) = C /\ B = D))))
8		opreq2 3007	. . . . . 6 |- (B = if(B e. NN0, B, 0) -> (if(A e. NN0, A, 0) + B) = (if(A e. NN0, A, 0) + if(B e. NN0, B, 0)))
9	8	opreq1d 3012	. . . . 5 |- (B = if(B e. NN0, B, 0) -> ((if(A e. NN0, A, 0) + B)^2) = ((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2))
10		id 9	. . . . 5 |- (B = if(B e. NN0, B, 0) -> B = if(B e. NN0, B, 0))
11	9, 10	opreq12d 3014	. . . 4 |- (B = if(B e. NN0, B, 0) -> (((if(A e. NN0, A, 0) + B)^2) + B) = (((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)))
12	11	cleq1d 1109	. . 3 |- (B = if(B e. NN0, B, 0) -> ((((if(A e. NN0, A, 0) + B)^2) + B) = (((C + D)^2) + D) <-> (((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((C + D)^2) + D)))
13		cleq1 1107	. . . 4 |- (B = if(B e. NN0, B, 0) -> (B = D <-> if(B e. NN0, B, 0) = D))
14	13	anbi2d 468	. . 3 |- (B = if(B e. NN0, B, 0) -> ((if(A e. NN0, A, 0) = C /\ B = D) <-> (if(A e. NN0, A, 0) = C /\ if(B e. NN0, B, 0) = D)))
15	12, 14	bibi12d 477	. 2 |- (B = if(B e. NN0, B, 0) -> (((((if(A e. NN0, A, 0) + B)^2) + B) = (((C + D)^2) + D) <-> (if(A e. NN0, A, 0) = C /\ B = D)) <-> ((((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((C + D)^2) + D) <-> (if(A e. NN0, A, 0) = C /\ if(B e. NN0, B, 0) = D))))
16		opreq1 3006	. . . . . 6 |- (C = if(C e. NN0, C, 0) -> (C + D) = (if(C e. NN0, C, 0) + D))
17	16	opreq1d 3012	. . . . 5 |- (C = if(C e. NN0, C, 0) -> ((C + D)^2) = ((if(C e. NN0, C, 0) + D)^2))
18	17	opreq1d 3012	. . . 4 |- (C = if(C e. NN0, C, 0) -> (((C + D)^2) + D) = (((if(C e. NN0, C, 0) + D)^2) + D))
19	18	cleq2d 1112	. . 3 |- (C = if(C e. NN0, C, 0) -> ((((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((C + D)^2) + D) <-> (((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((if(C e. NN0, C, 0) + D)^2) + D)))
20		cleq2 1110	. . . 4 |- (C = if(C e. NN0, C, 0) -> (if(A e. NN0, A, 0) = C <-> if(A e. NN0, A, 0) = if(C e. NN0, C, 0)))
21	20	anbi1d 469	. . 3 |- (C = if(C e. NN0, C, 0) -> ((if(A e. NN0, A, 0) = C /\ if(B e. NN0, B, 0) = D) <-> (if(A e. NN0, A, 0) = if(C e. NN0, C, 0) /\ if(B e. NN0, B, 0) = D)))
22	19, 21	bibi12d 477	. 2 |- (C = if(C e. NN0, C, 0) -> (((((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((C + D)^2) + D) <-> (if(A e. NN0, A, 0) = C /\ if(B e. NN0, B, 0) = D)) <-> ((((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((if(C e. NN0, C, 0) + D)^2) + D) <-> (if(A e. NN0, A, 0) = if(C e. NN0, C, 0) /\ if(B e. NN0, B, 0) = D))))
23		opreq2 3007	. . . . . 6 |- (D = if(D e. NN0, D, 0) -> (if(C e. NN0, C, 0) + D) = (if(C e. NN0, C, 0) + if(D e. NN0, D, 0)))
24	23	opreq1d 3012	. . . . 5 |- (D = if(D e. NN0, D, 0) -> ((if(C e. NN0, C, 0) + D)^2) = ((if(C e. NN0, C, 0) + if(D e. NN0, D, 0))^2))
25		id 9	. . . . 5 |- (D = if(D e. NN0, D, 0) -> D = if(D e. NN0, D, 0))
26	24, 25	opreq12d 3014	. . . 4 |- (D = if(D e. NN0, D, 0) -> (((if(C e. NN0, C, 0) + D)^2) + D) = (((if(C e. NN0, C, 0) + if(D e. NN0, D, 0))^2) + if(D e. NN0, D, 0)))
27	26	cleq2d 1112	. . 3 |- (D = if(D e. NN0, D, 0) -> ((((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((if(C e. NN0, C, 0) + D)^2) + D) <-> (((if(A e. NN0, A, 0) + if(B e. NN0, B, 0))^2) + if(B e. NN0, B, 0)) = (((if(C e. NN0, C, 0) + if(D e. NN0, D, 0))^2) + if(D e. NN0, D, 0))))
28		cleq2 1110	. . . 4 |- (D = if(D e. NN0, D, 0) -> (if(B e. NN0, B, 0) = D <-> if(B e. NN0, B, 0) = if(D e. NN0, D, 0)))
29	28	anbi2d 468	. . 3 |- (D = if(D e. NN0, D, 0) -> ((if(A e. NN0, A, 0) = if(C e. NN0, C, 0) /\ if(B e. NN0, B, 0) = D) <-> (if(A e. NN0, A, 0) = if(C e. NN0, C, 0) /\ if(B e.