Description: Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrmow , cbvrmovw when possible. (Contributed by NM, 16-Jun-2017) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvral.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| cbvral.2 | ⊢ Ⅎ 𝑥 𝜓 | ||
| cbvral.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | cbvrmo | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvral.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| 2 | cbvral.2 | ⊢ Ⅎ 𝑥 𝜓 | |
| 3 | cbvral.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 4 | 1 2 3 | cbvrex | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 ) |
| 5 | 1 2 3 | cbvreu | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ∈ 𝐴 𝜓 ) |
| 6 | 4 5 | imbi12i | ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝜓 → ∃! 𝑦 ∈ 𝐴 𝜓 ) ) |
| 7 | rmo5 | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) ) | |
| 8 | rmo5 | ⊢ ( ∃* 𝑦 ∈ 𝐴 𝜓 ↔ ( ∃ 𝑦 ∈ 𝐴 𝜓 → ∃! 𝑦 ∈ 𝐴 𝜓 ) ) | |
| 9 | 6 7 8 | 3bitr4i | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 ) |