Description: Transfer existence from a variable x to another variable y contained in expression A . (Contributed by NM, 10-Jun-2005) (Revised by Mario Carneiro, 15-Aug-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ralxfr.1 | ⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 ) | |
| ralxfr.2 | ⊢ ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) | ||
| ralxfr.3 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | ||
| Assertion | rexxfr | ⊢ ( ∃ 𝑥 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐶 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralxfr.1 | ⊢ ( 𝑦 ∈ 𝐶 → 𝐴 ∈ 𝐵 ) | |
| 2 | ralxfr.2 | ⊢ ( 𝑥 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) | |
| 3 | ralxfr.3 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| 4 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ 𝐵 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐵 ¬ 𝜑 ) | |
| 5 | dfrex2 | ⊢ ( ∃ 𝑦 ∈ 𝐶 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐶 ¬ 𝜓 ) | |
| 6 | 3 | notbid | ⊢ ( 𝑥 = 𝐴 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
| 7 | 1 2 6 | ralxfr | ⊢ ( ∀ 𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ∀ 𝑦 ∈ 𝐶 ¬ 𝜓 ) |
| 8 | 5 7 | xchbinxr | ⊢ ( ∃ 𝑦 ∈ 𝐶 𝜓 ↔ ¬ ∀ 𝑥 ∈ 𝐵 ¬ 𝜑 ) |
| 9 | 4 8 | bitr4i | ⊢ ( ∃ 𝑥 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐶 𝜓 ) |