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

Metamath Proof Explorer

Theorem rexnal2

Description: Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion rexnal2 ⊢ ∃ x ∈ A ∃ y ∈ B ¬ φ ↔ ¬ ∀ x ∈ A ∀ y ∈ B φ

Proof

Step Hyp Ref Expression
1 rexnal ⊢ ∃ y ∈ B ¬ φ ↔ ¬ ∀ y ∈ B φ
2 1 rexbii ⊢ ∃ x ∈ A ∃ y ∈ B ¬ φ ↔ ∃ x ∈ A ¬ ∀ y ∈ B φ
3 rexnal ⊢ ∃ x ∈ A ¬ ∀ y ∈ B φ ↔ ¬ ∀ x ∈ A ∀ y ∈ B φ
4 2 3 bitri ⊢ ∃ x ∈ A ∃ y ∈ B ¬ φ ↔ ¬ ∀ x ∈ A ∀ y ∈ B φ