eroveu

	Ref	Expression
Hypotheses	eropr.1	$⊢ J = A / R$
	eropr.2	$⊢ K = B / S$
	eropr.3	$⊢ φ \to T \in Z$
	eropr.4	$⊢ φ \to R Er U$
	eropr.5	$⊢ φ \to S Er V$
	eropr.6	$⊢ φ \to T Er W$
	eropr.7	$⊢ φ \to A \subseteq U$
	eropr.8	$⊢ φ \to B \subseteq V$
	eropr.9	$⊢ φ \to C \subseteq W$
	eropr.10	$⊢ φ \to \underset{˙}{+} : A \times B ⟶ C$
	eropr.11	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r R s \land t S u) \to (r \underset{˙}{+} t) T (s \underset{˙}{+} u))$
Assertion	eroveu	$⊢ (φ \land (X \in J \land Y \in K)) \to \exists! z \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$

Proof

Step	Hyp	Ref	Expression
1		eropr.1	$⊢ J = A / R$
2		eropr.2	$⊢ K = B / S$
3		eropr.3	$⊢ φ \to T \in Z$
4		eropr.4	$⊢ φ \to R Er U$
5		eropr.5	$⊢ φ \to S Er V$
6		eropr.6	$⊢ φ \to T Er W$
7		eropr.7	$⊢ φ \to A \subseteq U$
8		eropr.8	$⊢ φ \to B \subseteq V$
9		eropr.9	$⊢ φ \to C \subseteq W$
10		eropr.10	$⊢ φ \to \underset{˙}{+} : A \times B ⟶ C$
11		eropr.11	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r R s \land t S u) \to (r \underset{˙}{+} t) T (s \underset{˙}{+} u))$
12		elqsi	$⊢ X \in (A / R) \to \exists p \in A X = [p] R$
13	12 1	eleq2s	$⊢ X \in J \to \exists p \in A X = [p] R$
14		elqsi	$⊢ Y \in (B / S) \to \exists q \in B Y = [q] S$
15	14 2	eleq2s	$⊢ Y \in K \to \exists q \in B Y = [q] S$
16	13 15	anim12i	$⊢ (X \in J \land Y \in K) \to (\exists p \in A X = [p] R \land \exists q \in B Y = [q] S)$
17	16	adantl	$⊢ (φ \land (X \in J \land Y \in K)) \to (\exists p \in A X = [p] R \land \exists q \in B Y = [q] S)$
18		reeanv	$⊢ \exists p \in A \exists q \in B (X = [p] R \land Y = [q] S) \leftrightarrow (\exists p \in A X = [p] R \land \exists q \in B Y = [q] S)$
19	17 18	sylibr	$⊢ (φ \land (X \in J \land Y \in K)) \to \exists p \in A \exists q \in B (X = [p] R \land Y = [q] S)$
20	3	adantr	$⊢ (φ \land (X \in J \land Y \in K)) \to T \in Z$
21		ecexg	$⊢ T \in Z \to [(p \underset{˙}{+} q)] T \in V$
22		elisset	$⊢ [(p \underset{˙}{+} q)] T \in V \to \exists z z = [(p \underset{˙}{+} q)] T$
23	20 21 22	3syl	$⊢ (φ \land (X \in J \land Y \in K)) \to \exists z z = [(p \underset{˙}{+} q)] T$
24	23	biantrud	$⊢ (φ \land (X \in J \land Y \in K)) \to ((X = [p] R \land Y = [q] S) \leftrightarrow ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T))$
25	24	2rexbidv	$⊢ (φ \land (X \in J \land Y \in K)) \to (\exists p \in A \exists q \in B (X = [p] R \land Y = [q] S) \leftrightarrow \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T))$
26	19 25	mpbid	$⊢ (φ \land (X \in J \land Y \in K)) \to \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T)$
27		19.42v	$⊢ \exists z ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T)$
28	27	bicomi	$⊢ ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists z ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
29	28	rexbii	$⊢ \exists q \in B ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists q \in B \exists z ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
30		rexcom4	$⊢ \exists q \in B \exists z ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists z \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
31	29 30	bitri	$⊢ \exists q \in B ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists z \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
32	31	rexbii	$⊢ \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists p \in A \exists z \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
33		rexcom4	$⊢ \exists p \in A \exists z \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists z \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
34	32 33	bitri	$⊢ \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land \exists z z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists z \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
35	26 34	sylib	$⊢ (φ \land (X \in J \land Y \in K)) \to \exists z \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
36		reeanv	$⊢ \exists r \in A \exists s \in A (\exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \leftrightarrow (\exists r \in A \exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land \exists s \in A \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T))$
37		eceq1	$⊢ p = r \to [p] R = [r] R$
38	37	eqeq2d	$⊢ p = r \to (X = [p] R \leftrightarrow X = [r] R)$
39	38	anbi1d	$⊢ p = r \to ((X = [p] R \land Y = [q] S) \leftrightarrow (X = [r] R \land Y = [q] S))$
40		oveq1	$⊢ p = r \to p \underset{˙}{+} q = r \underset{˙}{+} q$
41	40	eceq1d	$⊢ p = r \to [(p \underset{˙}{+} q)] T = [(r \underset{˙}{+} q)] T$
42	41	eqeq2d	$⊢ p = r \to (z = [(p \underset{˙}{+} q)] T \leftrightarrow z = [(r \underset{˙}{+} q)] T)$
43	39 42	anbi12d	$⊢ p = r \to (((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow ((X = [r] R \land Y = [q] S) \land z = [(r \underset{˙}{+} q)] T))$
44		eceq1	$⊢ q = t \to [q] S = [t] S$
45	44	eqeq2d	$⊢ q = t \to (Y = [q] S \leftrightarrow Y = [t] S)$
46	45	anbi2d	$⊢ q = t \to ((X = [r] R \land Y = [q] S) \leftrightarrow (X = [r] R \land Y = [t] S))$
47		oveq2	$⊢ q = t \to r \underset{˙}{+} q = r \underset{˙}{+} t$
48	47	eceq1d	$⊢ q = t \to [(r \underset{˙}{+} q)] T = [(r \underset{˙}{+} t)] T$
49	48	eqeq2d	$⊢ q = t \to (z = [(r \underset{˙}{+} q)] T \leftrightarrow z = [(r \underset{˙}{+} t)] T)$
50	46 49	anbi12d	$⊢ q = t \to (((X = [r] R \land Y = [q] S) \land z = [(r \underset{˙}{+} q)] T) \leftrightarrow ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T))$
51	43 50	cbvrex2vw	$⊢ \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists r \in A \exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T)$
52		eceq1	$⊢ p = s \to [p] R = [s] R$
53	52	eqeq2d	$⊢ p = s \to (X = [p] R \leftrightarrow X = [s] R)$
54	53	anbi1d	$⊢ p = s \to ((X = [p] R \land Y = [q] S) \leftrightarrow (X = [s] R \land Y = [q] S))$
55		oveq1	$⊢ p = s \to p \underset{˙}{+} q = s \underset{˙}{+} q$
56	55	eceq1d	$⊢ p = s \to [(p \underset{˙}{+} q)] T = [(s \underset{˙}{+} q)] T$
57	56	eqeq2d	$⊢ p = s \to (w = [(p \underset{˙}{+} q)] T \leftrightarrow w = [(s \underset{˙}{+} q)] T)$
58	54 57	anbi12d	$⊢ p = s \to (((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T) \leftrightarrow ((X = [s] R \land Y = [q] S) \land w = [(s \underset{˙}{+} q)] T))$
59		eceq1	$⊢ q = u \to [q] S = [u] S$
60	59	eqeq2d	$⊢ q = u \to (Y = [q] S \leftrightarrow Y = [u] S)$
61	60	anbi2d	$⊢ q = u \to ((X = [s] R \land Y = [q] S) \leftrightarrow (X = [s] R \land Y = [u] S))$
62		oveq2	$⊢ q = u \to s \underset{˙}{+} q = s \underset{˙}{+} u$
63	62	eceq1d	$⊢ q = u \to [(s \underset{˙}{+} q)] T = [(s \underset{˙}{+} u)] T$
64	63	eqeq2d	$⊢ q = u \to (w = [(s \underset{˙}{+} q)] T \leftrightarrow w = [(s \underset{˙}{+} u)] T)$
65	61 64	anbi12d	$⊢ q = u \to (((X = [s] R \land Y = [q] S) \land w = [(s \underset{˙}{+} q)] T) \leftrightarrow ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T))$
66	58 65	cbvrex2vw	$⊢ \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists s \in A \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)$
67	51 66	anbi12i	$⊢ (\exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \land \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T)) \leftrightarrow (\exists r \in A \exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land \exists s \in A \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T))$
68	36 67	bitr4i	$⊢ \exists r \in A \exists s \in A (\exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \leftrightarrow (\exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \land \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T))$
69		reeanv	$⊢ \exists t \in B \exists u \in B (((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \leftrightarrow (\exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T))$
70	4	adantr	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to R Er U$
71	7	adantr	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to A \subseteq U$
72		simprll	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to r \in A$
73	71 72	sseldd	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to r \in U$
74	70 73	erth	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to (r R s \leftrightarrow [r] R = [s] R)$
75	5	adantr	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to S Er V$
76	8	adantr	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to B \subseteq V$
77		simprrl	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to t \in B$
78	76 77	sseldd	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to t \in V$
79	75 78	erth	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to (t S u \leftrightarrow [t] S = [u] S)$
80	74 79	anbi12d	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r R s \land t S u) \leftrightarrow ([r] R = [s] R \land [t] S = [u] S))$
81	6	adantr	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to T Er W$
82	9	adantr	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to C \subseteq W$
83	10	adantr	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to \underset{˙}{+} : A \times B ⟶ C$
84	83 72 77	fovcdmd	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to r \underset{˙}{+} t \in C$
85	82 84	sseldd	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to r \underset{˙}{+} t \in W$
86	81 85	erth	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r \underset{˙}{+} t) T (s \underset{˙}{+} u) \leftrightarrow [(r \underset{˙}{+} t)] T = [(s \underset{˙}{+} u)] T)$
87	11 80 86	3imtr3d	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to (([r] R = [s] R \land [t] S = [u] S) \to [(r \underset{˙}{+} t)] T = [(s \underset{˙}{+} u)] T)$
88		eqeq2	$⊢ w = [(s \underset{˙}{+} u)] T \to ([(r \underset{˙}{+} t)] T = w \leftrightarrow [(r \underset{˙}{+} t)] T = [(s \underset{˙}{+} u)] T)$
89	88	biimprcd	$⊢ [(r \underset{˙}{+} t)] T = [(s \underset{˙}{+} u)] T \to (w = [(s \underset{˙}{+} u)] T \to [(r \underset{˙}{+} t)] T = w)$
90	87 89	syl6	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to (([r] R = [s] R \land [t] S = [u] S) \to (w = [(s \underset{˙}{+} u)] T \to [(r \underset{˙}{+} t)] T = w))$
91	90	impd	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((([r] R = [s] R \land [t] S = [u] S) \land w = [(s \underset{˙}{+} u)] T) \to [(r \underset{˙}{+} t)] T = w)$
92		eqeq1	$⊢ X = [r] R \to (X = [s] R \leftrightarrow [r] R = [s] R)$
93		eqeq1	$⊢ Y = [t] S \to (Y = [u] S \leftrightarrow [t] S = [u] S)$
94	92 93	bi2anan9	$⊢ (X = [r] R \land Y = [t] S) \to ((X = [s] R \land Y = [u] S) \leftrightarrow ([r] R = [s] R \land [t] S = [u] S))$
95	94	anbi1d	$⊢ (X = [r] R \land Y = [t] S) \to (((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T) \leftrightarrow (([r] R = [s] R \land [t] S = [u] S) \land w = [(s \underset{˙}{+} u)] T))$
96	95	adantr	$⊢ ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \to (((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T) \leftrightarrow (([r] R = [s] R \land [t] S = [u] S) \land w = [(s \underset{˙}{+} u)] T))$
97		eqeq1	$⊢ z = [(r \underset{˙}{+} t)] T \to (z = w \leftrightarrow [(r \underset{˙}{+} t)] T = w)$
98	97	adantl	$⊢ ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \to (z = w \leftrightarrow [(r \underset{˙}{+} t)] T = w)$
99	96 98	imbi12d	$⊢ ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \to ((((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T) \to z = w) \leftrightarrow ((([r] R = [s] R \land [t] S = [u] S) \land w = [(s \underset{˙}{+} u)] T) \to [(r \underset{˙}{+} t)] T = w))$
100	91 99	syl5ibrcom	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to (((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \to (((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T) \to z = w))$
101	100	impd	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \to z = w)$
102	101	anassrs	$⊢ ((φ \land (r \in A \land s \in A)) \land (t \in B \land u \in B)) \to ((((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \to z = w)$
103	102	rexlimdvva	$⊢ (φ \land (r \in A \land s \in A)) \to (\exists t \in B \exists u \in B (((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \to z = w)$
104	69 103	biimtrrid	$⊢ (φ \land (r \in A \land s \in A)) \to ((\exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \to z = w)$
105	104	rexlimdvva	$⊢ φ \to (\exists r \in A \exists s \in A (\exists t \in B ((X = [r] R \land Y = [t] S) \land z = [(r \underset{˙}{+} t)] T) \land \exists u \in B ((X = [s] R \land Y = [u] S) \land w = [(s \underset{˙}{+} u)] T)) \to z = w)$
106	68 105	biimtrrid	$⊢ φ \to ((\exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \land \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T)) \to z = w)$
107	106	adantr	$⊢ (φ \land (X \in J \land Y \in K)) \to ((\exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \land \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T)) \to z = w)$
108	107	alrimivv	$⊢ (φ \land (X \in J \land Y \in K)) \to \forall z \forall w ((\exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \land \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T)) \to z = w)$
109		eqeq1	$⊢ z = w \to (z = [(p \underset{˙}{+} q)] T \leftrightarrow w = [(p \underset{˙}{+} q)] T)$
110	109	anbi2d	$⊢ z = w \to (((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T))$
111	110	2rexbidv	$⊢ z = w \to (\exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T))$
112	111	eu4	$⊢ \exists! z \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow (\exists z \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \land \forall z \forall w ((\exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \land \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land w = [(p \underset{˙}{+} q)] T)) \to z = w))$
113	35 108 112	sylanbrc	$⊢ (φ \land (X \in J \land Y \in K)) \to \exists! z \exists p \in A \exists q \in B ((X = [p] R \land Y = [q] S) \land z = [(p \underset{˙}{+} q)] T)$

Metamath Proof Explorer

Theorem eroveu

Proof