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 ⊢ Ⅎ y φ
cbvrmo.2 ⊢ Ⅎ x ψ
cbvrmo.3 ⊢ x = y → φ ↔ ψ
Assertion cbvreu ⊢ ∃! x ∈ A φ ↔ ∃! y ∈ A ψ

Proof

Step Hyp Ref Expression
1 cbvrmo.1 ⊢ Ⅎ y φ
2 cbvrmo.2 ⊢ Ⅎ x ψ
3 cbvrmo.3 ⊢ x = y → φ ↔ ψ
4 nfv ⊢ Ⅎ z x ∈ A ∧ φ
5 4 sb8eu ⊢ ∃! x x ∈ A ∧ φ ↔ ∃! z z x x ∈ A ∧ φ
6 sban ⊢ z x x ∈ A ∧ φ ↔ z x x ∈ A ∧ z x φ
7 6 eubii ⊢ ∃! z z x x ∈ A ∧ φ ↔ ∃! z z x x ∈ A ∧ z x φ
8 clelsb1 ⊢ z x x ∈ A ↔ z ∈ A
9 8 anbi1i ⊢ z x x ∈ A ∧ z x φ ↔ z ∈ A ∧ z x φ
10 9 eubii ⊢ ∃! z z x x ∈ A ∧ z x φ ↔ ∃! z z ∈ A ∧ z x φ
11 nfv ⊢ Ⅎ y z ∈ A
12 1 nfsb ⊢ Ⅎ y z x φ
13 11 12 nfan ⊢ Ⅎ y z ∈ A ∧ z x φ
14 nfv ⊢ Ⅎ z y ∈ A ∧ ψ
15 eleq1w ⊢ z = y → z ∈ A ↔ y ∈ A
16 sbequ ⊢ z = y → z x φ ↔ y x φ
17 2 3 sbie ⊢ y x φ ↔ ψ
18 16 17 bitrdi ⊢ z = y → z x φ ↔ ψ
19 15 18 anbi12d ⊢ z = y → z ∈ A ∧ z x φ ↔ y ∈ A ∧ ψ
20 13 14 19 cbveu ⊢ ∃! z z ∈ A ∧ z x φ ↔ ∃! y y ∈ A ∧ ψ
21 10 20 bitri ⊢ ∃! z z x x ∈ A ∧ z x φ ↔ ∃! y y ∈ A ∧ ψ
22 5 7 21 3bitri ⊢ ∃! x x ∈ A ∧ φ ↔ ∃! y y ∈ A ∧ ψ
23 df-reu ⊢ ∃! x ∈ A φ ↔ ∃! x x ∈ A ∧ φ
24 df-reu ⊢ ∃! y ∈ A ψ ↔ ∃! y y ∈ A ∧ ψ
25 22 23 24 3bitr4i ⊢ ∃! x ∈ A φ ↔ ∃! y ∈ A ψ