Description: Rule used to change bound variables, using implicit substitution. Version of cbvex4v with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995) Avoid ax-13 . (Revised by GG, 10-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvex4vw.1 | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( 𝜑 ↔ 𝜓 ) ) | |
| cbvex4vw.2 | ⊢ ( ( 𝑧 = 𝑓 ∧ 𝑤 = 𝑔 ) → ( 𝜓 ↔ 𝜒 ) ) | ||
| Assertion | cbvex4vw | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvex4vw.1 | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | cbvex4vw.2 | ⊢ ( ( 𝑧 = 𝑓 ∧ 𝑤 = 𝑔 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| 3 | 1 | 2exbidv | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜓 ) ) |
| 4 | 3 | cbvex2vw | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑧 ∃ 𝑤 𝜓 ) |
| 5 | 2 | cbvex2vw | ⊢ ( ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑓 ∃ 𝑔 𝜒 ) |
| 6 | 5 | 2exbii | ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |
| 7 | 4 6 | bitri | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |