Theorem cbveud

Description: Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021)

	Ref	Expression
Hypotheses	cbveud.1	⊢ Ⅎ 𝑥 𝜑
	cbveud.2	⊢ Ⅎ 𝑦 𝜑
	cbveud.3	⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
	cbveud.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	cbveud.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
Assertion	cbveud	⊢ ( 𝜑 → ( ∃! 𝑥 𝜓 ↔ ∃! 𝑦 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		cbveud.1	⊢ Ⅎ 𝑥 𝜑
2		cbveud.2	⊢ Ⅎ 𝑦 𝜑
3		cbveud.3	⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
4		cbveud.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
5		cbveud.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
6		nfvd	⊢ ( 𝜑 → Ⅎ 𝑦 𝑥 = 𝑧 )
7	3 6	nfbid	⊢ ( 𝜑 → Ⅎ 𝑦 ( 𝜓 ↔ 𝑥 = 𝑧 ) )
8		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 = 𝑧 )
9	4 8	nfbid	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝜒 ↔ 𝑦 = 𝑧 ) )
10		simpr	⊢ ( ( 𝑥 = 𝑦 ∧ ( 𝜓 ↔ 𝜒 ) ) → ( 𝜓 ↔ 𝜒 ) )
11		equequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )
12	11	adantr	⊢ ( ( 𝑥 = 𝑦 ∧ ( 𝜓 ↔ 𝜒 ) ) → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )
13	10 12	bibi12d	⊢ ( ( 𝑥 = 𝑦 ∧ ( 𝜓 ↔ 𝜒 ) ) → ( ( 𝜓 ↔ 𝑥 = 𝑧 ) ↔ ( 𝜒 ↔ 𝑦 = 𝑧 ) ) )
14	13	ex	⊢ ( 𝑥 = 𝑦 → ( ( 𝜓 ↔ 𝜒 ) → ( ( 𝜓 ↔ 𝑥 = 𝑧 ) ↔ ( 𝜒 ↔ 𝑦 = 𝑧 ) ) ) )
15	5 14	sylcom	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( ( 𝜓 ↔ 𝑥 = 𝑧 ) ↔ ( 𝜒 ↔ 𝑦 = 𝑧 ) ) ) )
16	1 2 7 9 15	cbv2w	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ( 𝜒 ↔ 𝑦 = 𝑧 ) ) )
17	16	exbidv	⊢ ( 𝜑 → ( ∃ 𝑧 ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜒 ↔ 𝑦 = 𝑧 ) ) )
18		eu6	⊢ ( ∃! 𝑥 𝜓 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) )
19		eu6	⊢ ( ∃! 𝑦 𝜒 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜒 ↔ 𝑦 = 𝑧 ) )
20	17 18 19	3bitr4g	⊢ ( 𝜑 → ( ∃! 𝑥 𝜓 ↔ ∃! 𝑦 𝜒 ) )