Theorem 2reuimp0 44606

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 3668	. . 3 ⊢ (∃!𝑏 ∈ 𝑉 𝜑 ↔ ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)))
3	2	reubii 3325	. 2 ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 ↔ ∃!𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)))
4		2reuimp.d	. . . . . 6 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜒))
5		2reuimp.a	. . . . . . . 8 ⊢ (𝑎 = 𝑑 → (𝜃 ↔ 𝜏))
6	5	imbi1d 342	. . . . . . 7 ⊢ (𝑎 = 𝑑 → ((𝜃 → 𝑏 = 𝑐) ↔ (𝜏 → 𝑏 = 𝑐)))
7	6	ralbidv 3112	. . . . . 6 ⊢ (𝑎 = 𝑑 → (∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)))
8	4, 7	anbi12d 631	. . . . 5 ⊢ (𝑎 = 𝑑 → ((𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐))))
9	8	rexbidv 3226	. . . 4 ⊢ (𝑎 = 𝑑 → (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ ∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐))))
10	9	reu8 3668	. . 3 ⊢ (∃!𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ ∃𝑎 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)))
11		r19.28v 3116	. . . . 5 ⊢ ((∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)))
12		2reuimp.e	. . . . . . . . . 10 ⊢ (𝑏 = 𝑒 → (𝜑 ↔ 𝜂))
13		equequ1 2028	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (𝑏 = 𝑐 ↔ 𝑒 = 𝑐))
14	13	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → ((𝜃 → 𝑏 = 𝑐) ↔ (𝜃 → 𝑒 = 𝑐)))
15	14	ralbidv 3112	. . . . . . . . . 10 ⊢ (𝑏 = 𝑒 → (∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐) ↔ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)))
16	12, 15	anbi12d 631	. . . . . . . . 9 ⊢ (𝑏 = 𝑒 → ((𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
17	16	cbvrexvw 3384	. . . . . . . 8 ⊢ (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ↔ ∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)))
18		r19.23v 3208	. . . . . . . . 9 ⊢ (∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ↔ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑))
19		r19.28v 3116	. . . . . . . . . . 11 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)))
20		ancom 461	. . . . . . . . . . . . . 14 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
21		r19.42v 3279	. . . . . . . . . . . . . 14 ⊢ (∃𝑒 ∈ 𝑉 (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))) ↔ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ ∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
22	20, 21	bitr4i 277	. . . . . . . . . . . . 13 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ↔ ∃𝑒 ∈ 𝑉 (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))))
23		2reuimp.f	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜓))
24		equequ2 2029	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑓 → (𝑒 = 𝑐 ↔ 𝑒 = 𝑓))
25	23, 24	imbi12d 345	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑓 → ((𝜃 → 𝑒 = 𝑐) ↔ (𝜓 → 𝑒 = 𝑓)))
26	25	cbvralvw 3383	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐) ↔ ∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓))
27		r19.28v 3116	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ ∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓)) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
28	27	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → (∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
29	28	expcom 414	. . . . . . . . . . . . . . . 16 ⊢ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑓 ∈ 𝑉 (𝜓 → 𝑒 = 𝑓) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))))
30	26, 29	syl7bi 254	. . . . . . . . . . . . . . 15 ⊢ (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → (𝜂 → (∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))))
31	30	imp32 419	. . . . . . . . . . . . . 14 ⊢ ((((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))) → ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
32	31	reximi 3178	. . . . . . . . . . . . 13 ⊢ (∃𝑒 ∈ 𝑉 (((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) ∧ (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐))) → ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
33	22, 32	sylbi 216	. . . . . . . . . . . 12 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
34	33	ralimi 3087	. . . . . . . . . . 11 ⊢ (∀𝑏 ∈ 𝑉 (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
35	19, 34	syl 17	. . . . . . . . . 10 ⊢ ((∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) ∧ ∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
36	35	ex 413	. . . . . . . . 9 ⊢ (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) → (∀𝑏 ∈ 𝑉 ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
37	18, 36	syl5bir 242	. . . . . . . 8 ⊢ (∃𝑒 ∈ 𝑉 (𝜂 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑒 = 𝑐)) → ((∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
38	17, 37	sylbi 216	. . . . . . 7 ⊢ (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) → ((∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓))))
39	38	imp 407	. . . . . 6 ⊢ ((∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
40	39	ralimi 3087	. . . . 5 ⊢ (∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
41	11, 40	syl 17	. . . 4 ⊢ ((∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
42	41	reximi 3178	. . 3 ⊢ (∃𝑎 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) ∧ ∀𝑑 ∈ 𝑉 (∃𝑏 ∈ 𝑉 (𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
43	10, 42	sylbi 216	. 2 ⊢ (∃!𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝜑 ∧ ∀𝑐 ∈ 𝑉 (𝜃 → 𝑏 = 𝑐)) → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))
44	3, 43	sylbi 216	1 ⊢ (∃!𝑎 ∈ 𝑉 ∃!𝑏 ∈ 𝑉 𝜑 → ∃𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ∃𝑒 ∈ 𝑉 ∀𝑓 ∈ 𝑉 ((𝜂 ∧ ((𝜒 ∧ ∀𝑐 ∈ 𝑉 (𝜏 → 𝑏 = 𝑐)) → 𝑎 = 𝑑)) ∧ (𝜓 → 𝑒 = 𝑓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-10 2137  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clel 2816  df-ral 3069  df-rex 3070  df-reu 3072

This theorem is referenced by:  2reuimp  44607