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

Metamath Proof Explorer

Theorem ralinexa

Description: A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005)

Ref Expression
Assertion ralinexa ⊢ ∀ x ∈ A φ → ¬ ψ ↔ ¬ ∃ x ∈ A φ ∧ ψ

Proof

Step Hyp Ref Expression
1 imnan ⊢ φ → ¬ ψ ↔ ¬ φ ∧ ψ
2 1 ralbii ⊢ ∀ x ∈ A φ → ¬ ψ ↔ ∀ x ∈ A ¬ φ ∧ ψ
3 ralnex ⊢ ∀ x ∈ A ¬ φ ∧ ψ ↔ ¬ ∃ x ∈ A φ ∧ ψ
4 2 3 bitri ⊢ ∀ x ∈ A φ → ¬ ψ ↔ ¬ ∃ x ∈ A φ ∧ ψ