This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nrexralim

Description: Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009)

Ref Expression
Assertion nrexralim ⊢ ¬ ∃ x ∈ A ∀ y ∈ B φ → ψ ↔ ∀ x ∈ A ∃ y ∈ B φ ∧ ¬ ψ

Proof

Step Hyp Ref Expression
1 rexanali ⊢ ∃ y ∈ B φ ∧ ¬ ψ ↔ ¬ ∀ y ∈ B φ → ψ
2 1 ralbii ⊢ ∀ x ∈ A ∃ y ∈ B φ ∧ ¬ ψ ↔ ∀ x ∈ A ¬ ∀ y ∈ B φ → ψ
3 ralnex ⊢ ∀ x ∈ A ¬ ∀ y ∈ B φ → ψ ↔ ¬ ∃ x ∈ A ∀ y ∈ B φ → ψ
4 2 3 bitr2i ⊢ ¬ ∃ x ∈ A ∀ y ∈ B φ → ψ ↔ ∀ x ∈ A ∃ y ∈ B φ ∧ ¬ ψ