Description: Transfer existential quantification from a variable x to another variable y contained in expression A . (Contributed by Mario Carneiro, 20-Aug-2014) (Proof shortened by Mario Carneiro, 19-Nov-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ralxfr2d.1 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝑉 ) | |
| ralxfr2d.2 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) ) | ||
| ralxfr2d.3 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) ) | ||
| Assertion | rexxfr2d | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ∃ 𝑦 ∈ 𝐶 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralxfr2d.1 | ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝑉 ) | |
| 2 | ralxfr2d.2 | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ) ) | |
| 3 | ralxfr2d.3 | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| 4 | 3 | notbid | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ¬ 𝜓 ↔ ¬ 𝜒 ) ) |
| 5 | 1 2 4 | ralxfr2d | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ¬ 𝜓 ↔ ∀ 𝑦 ∈ 𝐶 ¬ 𝜒 ) ) |
| 6 | 5 | notbid | ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 ∈ 𝐵 ¬ 𝜓 ↔ ¬ ∀ 𝑦 ∈ 𝐶 ¬ 𝜒 ) ) |
| 7 | dfrex2 | ⊢ ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ¬ ∀ 𝑥 ∈ 𝐵 ¬ 𝜓 ) | |
| 8 | dfrex2 | ⊢ ( ∃ 𝑦 ∈ 𝐶 𝜒 ↔ ¬ ∀ 𝑦 ∈ 𝐶 ¬ 𝜒 ) | |
| 9 | 6 7 8 | 3bitr4g | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ∃ 𝑦 ∈ 𝐶 𝜒 ) ) |