Description: Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009)
Ref | Expression | ||
---|---|---|---|
Assertion | nrexralim | ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ¬ 𝜓 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexanali | ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ¬ 𝜓 ) ↔ ¬ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ) | |
2 | 1 | ralbii | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ¬ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ) |
3 | ralnex | ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ) | |
4 | 2 3 | bitr2i | ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ¬ 𝜓 ) ) |