Theorem cbvreuw

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvreuw.1	⊢ Ⅎ 𝑦 𝜑
2		cbvreuw.2	⊢ Ⅎ 𝑥 𝜓
3		cbvreuw.3	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
4		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
5	4	sb8euv	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑧 [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
6		sban	⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
7	6	eubii	⊢ ( ∃! 𝑧 [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
8		clelsb1	⊢ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 )
9	8	anbi1i	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
10	9	eubii	⊢ ( ∃! 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∃! 𝑧 ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
11		nfv	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐴
12	1	nfsbv	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
13	11 12	nfan	⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
14		nfv	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐴 ∧ 𝜓 )
15		eleq1w	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
16		sbequ	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
17	2 3	sbiev	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
18	16 17	bitrdi	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
19	15 18	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
20	13 14 19	cbveuw	⊢ ( ∃! 𝑧 ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
21	10 20	bitri	⊢ ( ∃! 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
22	5 7 21	3bitri	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
23		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
24		df-reu	⊢ ( ∃! 𝑦 ∈ 𝐴 𝜓 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
25	22 23 24	3bitr4i	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ∈ 𝐴 𝜓 )