Description: Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrex2vw when possible. (Contributed by FL, 2-Jul-2012) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cbvrex2v.1 | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜒 ) ) | |
| cbvrex2v.2 | ⊢ ( 𝑦 = 𝑤 → ( 𝜒 ↔ 𝜓 ) ) | ||
| Assertion | cbvrex2v | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvrex2v.1 | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜒 ) ) | |
| 2 | cbvrex2v.2 | ⊢ ( 𝑦 = 𝑤 → ( 𝜒 ↔ 𝜓 ) ) | |
| 3 | 1 | rexbidv | ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 𝜒 ) ) |
| 4 | 3 | cbvrexv | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 ) |
| 5 | 2 | cbvrexv | ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜒 ↔ ∃ 𝑤 ∈ 𝐵 𝜓 ) |
| 6 | 5 | rexbii | ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜒 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝜓 ) |
| 7 | 4 6 | bitri | ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝜓 ) |