Theorem 2reuimp0 48153

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023.)

Hypotheses

Ref	Expression
2reuimp.c	⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃))
2reuimp.d	⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))
2reuimp.a	⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))
2reuimp.e	⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))
2reuimp.f	⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))

Assertion

Ref	Expression
2reuimp0	⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))

Distinct variable groups:   𝑉,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝜑,𝑐,𝑑,𝑒   𝜃,𝑏,𝑑,𝑒,𝑓   𝜒,𝑎,𝑒,𝑓   𝜏,𝑎,𝑒,𝑓   𝜂,𝑏,𝑓   𝜓,𝑐

Allowed substitution hints:   𝜑(𝑓, 𝑎, 𝑏)   𝜓(𝑒, 𝑓, 𝑎, 𝑏, 𝑑)   𝜒(𝑏, 𝑐, 𝑑)   𝜃(𝑎, 𝑐)   𝜏(𝑏, 𝑐, 𝑑)   𝜂(𝑒, 𝑎, 𝑐, 𝑑)

Proof of Theorem 2reuimp0

Step	Hyp	Ref	Expression
1		2reuimp.c	. . . 4 ⊢ (𝑏 = 𝑐 → (𝜑 ↔ 𝜃))
2	1	reu8 3691	. . 3 ⊢ (∃!𝑏 ∈ 𝑉 𝜑 ↔ ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)))
3	2	reubii 3375	. 2 ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 ↔ ∃!𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)))
4		2reuimp.d	. . . . . 6 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))
5		2reuimp.a	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))
6	5	imbi1d 344	. . . . . . 7 ⊢ (𝑎 = 𝑑 → ((𝜃 → 𝑏 = 𝑐) ↔ (𝜏 → 𝑏 = 𝑐)))
7	6	ralbidv 3186	. . . . . 6 ⊢ (𝑎 = 𝑑 → (∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)))
8	4, 7	anbi12d 644	. . . . 5 ⊢ (𝑎 = 𝑑 → ((𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐))))
9	8	rexbidv 3187	. . . 4 ⊢ (𝑎 = 𝑑 → (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ ∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐))))
10	9	reu8 3691	. . 3 ⊢ (∃!𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ ∃𝑎 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)))
11		r19.28v 3194	. . . . 5 ⊢ ((∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)))
12		2reuimp.e	. . . . . . . . . 10 ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))
13		equequ1 2058	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (𝑏 = 𝑐 ↔ 𝑒 = 𝑐))
14	13	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → ((𝜃 → 𝑏 = 𝑐) ↔ (𝜃 → 𝑒 = 𝑐)))
15	14	ralbidv 3186	. . . . . . . . . 10 ⊢ (𝑏 = 𝑒 → (∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)))
16	12, 15	anbi12d 644	. . . . . . . . 9 ⊢ (𝑏 = 𝑒 → ((𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
17	16	cbvrexvw 3242	. . . . . . . 8 ⊢ (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ ∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)))
18		r19.23v 3190	. . . . . . . . 9 ⊢ (∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ↔ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑))
19		r19.28v 3194	. . . . . . . . . . 11 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)))
20		ancom 466	. . . . . . . . . . . . . 14 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
21		r19.42v 3195	. . . . . . . . . . . . . 14 ⊢ (∃𝑒 ∈ 𝑉 (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))) ↔ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
22	20, 21	bitr4i 281	. . . . . . . . . . . . 13 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ ∃𝑒 ∈ 𝑉 (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
23		2reuimp.f	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))
24		equequ2 2059	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑓 → (𝑒 = 𝑐 ↔ 𝑒 = 𝑓))
25	23, 24	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑓 → ((𝜃 → 𝑒 = 𝑐) ↔ (𝜓 → 𝑒 = 𝑓)))
26	25	cbvralvw 3241	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐) ↔ ∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓))
27		r19.28v 3194	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ ∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓)) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
28	27	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → (∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
29	28	expcom 419	. . . . . . . . . . . . . . . 16 ⊢ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))))
30	26, 29	syl7bi 258	. . . . . . . . . . . . . . 15 ⊢ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))))
31	30	imp32 424	. . . . . . . . . . . . . 14 ⊢ ((((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
32	31	reximi 3101	. . . . . . . . . . . . 13 ⊢ (∃𝑒 ∈ 𝑉 (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))) → ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
33	22, 32	sylbi 220	. . . . . . . . . . . 12 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
34	33	ralimi 3100	. . . . . . . . . . 11 ⊢ (∀𝑏 ∈ 𝑉 (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
35	19, 34	syl 18	. . . . . . . . . 10 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
36	35	ex 418	. . . . . . . . 9 ⊢ (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) → (∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
37	18, 36	biimtrrid 246	. . . . . . . 8 ⊢ (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) → ((∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
38	17, 37	sylbi 220	. . . . . . 7 ⊢ (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) → ((∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
39	38	imp 412	. . . . . 6 ⊢ ((∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
40	39	ralimi 3100	. . . . 5 ⊢ (∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
41	11, 40	syl 18	. . . 4 ⊢ ((∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
42	41	reximi 3101	. . 3 ⊢ (∃𝑎 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
43	10, 42	sylbi 220	. 2 ⊢ (∃!𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
44	3, 43	sylbi 220	1 ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-10 2178  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clel 2836  df-ral 3078  df-rex 3088  df-reu 3367

This theorem is used by:  2reuimp  48154