Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvex4vw if possible. (Contributed by NM, 26-Jul-1995) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvex4v.1 | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( 𝜑 ↔ 𝜓 ) ) | |
| cbvex4v.2 | ⊢ ( ( 𝑧 = 𝑓 ∧ 𝑤 = 𝑔 ) → ( 𝜓 ↔ 𝜒 ) ) | ||
| Assertion | cbvex4v | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvex4v.1 | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | cbvex4v.2 | ⊢ ( ( 𝑧 = 𝑓 ∧ 𝑤 = 𝑔 ) → ( 𝜓 ↔ 𝜒 ) ) | |
| 3 | 1 | 2exbidv | ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑢 ) → ( ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 𝜓 ) ) |
| 4 | 3 | cbvex2vv | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑧 ∃ 𝑤 𝜓 ) |
| 5 | 2 | cbvex2vv | ⊢ ( ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑓 ∃ 𝑔 𝜒 ) |
| 6 | 5 | 2exbii | ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑧 ∃ 𝑤 𝜓 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |
| 7 | 4 6 | bitri | ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 𝜑 ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑓 ∃ 𝑔 𝜒 ) |