reu2eqd

Description: Deduce equality from restricted uniqueness, deduction version. (Contributed by Thierry Arnoux, 27-Nov-2019)

	Ref	Expression
Hypotheses	reu2eqd.1	$⊢ x = B \to (ψ \leftrightarrow χ)$
	reu2eqd.2	$⊢ x = C \to (ψ \leftrightarrow θ)$
	reu2eqd.3	$⊢ φ \to \exists! x \in A ψ$
	reu2eqd.4	$⊢ φ \to B \in A$
	reu2eqd.5	$⊢ φ \to C \in A$
	reu2eqd.6	$⊢ φ \to χ$
	reu2eqd.7	$⊢ φ \to θ$
Assertion	reu2eqd	$⊢ φ \to B = C$

Proof

Step	Hyp	Ref	Expression
1		reu2eqd.1	$⊢ x = B \to (ψ \leftrightarrow χ)$
2		reu2eqd.2	$⊢ x = C \to (ψ \leftrightarrow θ)$
3		reu2eqd.3	$⊢ φ \to \exists! x \in A ψ$
4		reu2eqd.4	$⊢ φ \to B \in A$
5		reu2eqd.5	$⊢ φ \to C \in A$
6		reu2eqd.6	$⊢ φ \to χ$
7		reu2eqd.7	$⊢ φ \to θ$
8		reu2	$⊢ \exists! x \in A ψ \leftrightarrow (\exists x \in A ψ \land \forall x \in A \forall y \in A ((ψ \land [y/ x] ψ) \to x = y))$
9	3 8	sylib	$⊢ φ \to (\exists x \in A ψ \land \forall x \in A \forall y \in A ((ψ \land [y/ x] ψ) \to x = y))$
10	9	simprd	$⊢ φ \to \forall x \in A \forall y \in A ((ψ \land [y/ x] ψ) \to x = y)$
11		nfv	$⊢ Ⅎ x χ$
12		nfs1v	$⊢ Ⅎ x [y/ x] ψ$
13	11 12	nfan	$⊢ Ⅎ x (χ \land [y/ x] ψ)$
14		nfv	$⊢ Ⅎ x B = y$
15	13 14	nfim	$⊢ Ⅎ x ((χ \land [y/ x] ψ) \to B = y)$
16		nfv	$⊢ Ⅎ y ((χ \land θ) \to B = C)$
17	1	anbi1d	$⊢ x = B \to ((ψ \land [y/ x] ψ) \leftrightarrow (χ \land [y/ x] ψ))$
18		eqeq1	$⊢ x = B \to (x = y \leftrightarrow B = y)$
19	17 18	imbi12d	$⊢ x = B \to (((ψ \land [y/ x] ψ) \to x = y) \leftrightarrow ((χ \land [y/ x] ψ) \to B = y))$
20		nfv	$⊢ Ⅎ x θ$
21	20 2	sbhypf	$⊢ y = C \to ([y/ x] ψ \leftrightarrow θ)$
22	21	anbi2d	$⊢ y = C \to ((χ \land [y/ x] ψ) \leftrightarrow (χ \land θ))$
23		eqeq2	$⊢ y = C \to (B = y \leftrightarrow B = C)$
24	22 23	imbi12d	$⊢ y = C \to (((χ \land [y/ x] ψ) \to B = y) \leftrightarrow ((χ \land θ) \to B = C))$
25	15 16 19 24	rspc2	$⊢ (B \in A \land C \in A) \to (\forall x \in A \forall y \in A ((ψ \land [y/ x] ψ) \to x = y) \to ((χ \land θ) \to B = C))$
26	4 5 25	syl2anc	$⊢ φ \to (\forall x \in A \forall y \in A ((ψ \land [y/ x] ψ) \to x = y) \to ((χ \land θ) \to B = C))$
27	10 26	mpd	$⊢ φ \to ((χ \land θ) \to B = C)$
28	6 7 27	mp2and	$⊢ φ \to B = C$

Metamath Proof Explorer

Theorem reu2eqd

Proof