Description: Obsolete version of cbvrmow as of 23-May-2024. (Contributed by NM, 16-Jun-2017) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvrmowOLD.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| cbvrmowOLD.2 | ⊢ Ⅎ 𝑥 𝜓 | ||
| cbvrmowOLD.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | cbvrmowOLD | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvrmowOLD.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| 2 | cbvrmowOLD.2 | ⊢ Ⅎ 𝑥 𝜓 | |
| 3 | cbvrmowOLD.3 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 4 | 1 2 3 | cbvrexw | ⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 ∈ 𝐴 𝜓 ) |
| 5 | 1 2 3 | cbvreuw | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ∈ 𝐴 𝜓 ) |
| 6 | 4 5 | imbi12i | ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃ 𝑦 ∈ 𝐴 𝜓 → ∃! 𝑦 ∈ 𝐴 𝜓 ) ) |
| 7 | rmo5 | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) ) | |
| 8 | rmo5 | ⊢ ( ∃* 𝑦 ∈ 𝐴 𝜓 ↔ ( ∃ 𝑦 ∈ 𝐴 𝜓 → ∃! 𝑦 ∈ 𝐴 𝜓 ) ) | |
| 9 | 6 7 8 | 3bitr4i | ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑦 ∈ 𝐴 𝜓 ) |