Description: Obsolete version of ralcom3 as of 22-Dec-2024. (Contributed by NM, 22-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ralcom3OLD | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.04 | ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 → 𝜑 ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ) | |
| 2 | 1 | ralimi2 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝜑 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
| 3 | pm2.04 | ⊢ ( ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐵 → 𝜑 ) ) ) | |
| 4 | 3 | ralimi2 | ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝜑 ) ) |
| 5 | 2 4 | impbii | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |