This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvreu

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvreuw when possible. (Contributed by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

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

Proof

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