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 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |