reu2eqd

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

	Ref	Expression
Hypotheses	reu2eqd.1	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	reu2eqd.2	⊢ ( 𝑥 = 𝐶 → ( 𝜓 ↔ 𝜃 ) )
	reu2eqd.3	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜓 )
	reu2eqd.4	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	reu2eqd.5	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
	reu2eqd.6	⊢ ( 𝜑 → 𝜒 )
	reu2eqd.7	⊢ ( 𝜑 → 𝜃 )
Assertion	reu2eqd	⊢ ( 𝜑 → 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		reu2eqd.1	⊢ ( 𝑥 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
2		reu2eqd.2	⊢ ( 𝑥 = 𝐶 → ( 𝜓 ↔ 𝜃 ) )
3		reu2eqd.3	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜓 )
4		reu2eqd.4	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
5		reu2eqd.5	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
6		reu2eqd.6	⊢ ( 𝜑 → 𝜒 )
7		reu2eqd.7	⊢ ( 𝜑 → 𝜃 )
8		reu2	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝑥 = 𝑦 ) ) )
9	3 8	sylib	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝑥 = 𝑦 ) ) )
10	9	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝑥 = 𝑦 ) )
11		nfv	⊢ Ⅎ 𝑥 𝜒
12		nfs1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜓
13	11 12	nfan	⊢ Ⅎ 𝑥 ( 𝜒 ∧ [ 𝑦 / 𝑥 ] 𝜓 )
14		nfv	⊢ Ⅎ 𝑥 𝐵 = 𝑦
15	13 14	nfim	⊢ Ⅎ 𝑥 ( ( 𝜒 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝐵 = 𝑦 )
16		nfv	⊢ Ⅎ 𝑦 ( ( 𝜒 ∧ 𝜃 ) → 𝐵 = 𝐶 )
17	1	anbi1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝜒 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ) )
18		eqeq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝑦 ↔ 𝐵 = 𝑦 ) )
19	17 18	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝜒 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝐵 = 𝑦 ) ) )
20		nfv	⊢ Ⅎ 𝑥 𝜃
21	20 2	sbhypf	⊢ ( 𝑦 = 𝐶 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜃 ) )
22	21	anbi2d	⊢ ( 𝑦 = 𝐶 → ( ( 𝜒 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝜒 ∧ 𝜃 ) ) )
23		eqeq2	⊢ ( 𝑦 = 𝐶 → ( 𝐵 = 𝑦 ↔ 𝐵 = 𝐶 ) )
24	22 23	imbi12d	⊢ ( 𝑦 = 𝐶 → ( ( ( 𝜒 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝐵 = 𝑦 ) ↔ ( ( 𝜒 ∧ 𝜃 ) → 𝐵 = 𝐶 ) ) )
25	15 16 19 24	rspc2	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝑥 = 𝑦 ) → ( ( 𝜒 ∧ 𝜃 ) → 𝐵 = 𝐶 ) ) )
26	4 5 25	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜓 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → 𝑥 = 𝑦 ) → ( ( 𝜒 ∧ 𝜃 ) → 𝐵 = 𝐶 ) ) )
27	10 26	mpd	⊢ ( 𝜑 → ( ( 𝜒 ∧ 𝜃 ) → 𝐵 = 𝐶 ) )
28	6 7 27	mp2and	⊢ ( 𝜑 → 𝐵 = 𝐶 )

Metamath Proof Explorer

Theorem reu2eqd

Proof