Theorem cbvreud

Description: Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		cbvreud.1	⊢ Ⅎ 𝑥 𝜑
2		cbvreud.2	⊢ Ⅎ 𝑦 𝜑
3		cbvreud.3	⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
4		cbvreud.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
5		cbvreud.5	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
6		nfvd	⊢ ( 𝜑 → Ⅎ 𝑦 𝑥 ∈ 𝐴 )
7	6 3	nfand	⊢ ( 𝜑 → Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
8		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
9	8 4	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜒 ) )
10		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
12	5	imp	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
13	11 12	anbi12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜒 ) ) )
14	13	ex	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜒 ) ) ) )
15	1 2 7 9 14	cbveud	⊢ ( 𝜑 → ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜒 ) ) )
16		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
17		df-reu	⊢ ( ∃! 𝑦 ∈ 𝐴 𝜒 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜒 ) )
18	15 16 17	3bitr4g	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑦 ∈ 𝐴 𝜒 ) )