Description: Change bound variables of triple restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvral3vw when possible. (Contributed by NM, 10-May-2005) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvral3v.1 | ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) ) | |
| cbvral3v.2 | ⊢ ( 𝑦 = 𝑣 → ( 𝜒 ↔ 𝜃 ) ) | ||
| cbvral3v.3 | ⊢ ( 𝑧 = 𝑢 → ( 𝜃 ↔ 𝜓 ) ) | ||
| Assertion | cbvral3v | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvral3v.1 | ⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) ) | |
| 2 | cbvral3v.2 | ⊢ ( 𝑦 = 𝑣 → ( 𝜒 ↔ 𝜃 ) ) | |
| 3 | cbvral3v.3 | ⊢ ( 𝑧 = 𝑢 → ( 𝜃 ↔ 𝜓 ) ) | |
| 4 | 1 | 2ralbidv | ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 ) ) |
| 5 | 4 | cbvralv | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 ) |
| 6 | 2 3 | cbvral2v | ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 ↔ ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 ) |
| 7 | 6 | ralbii | ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 ) |
| 8 | 5 7 | bitri | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 ) |