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

Metamath Proof Explorer

Theorem r2exlem

Description: Lemma factoring out common proof steps in r2exf an r2ex . Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020)

Ref Expression
Hypothesis r2exlem.1 ⊢ ∀ x ∈ A ∀ y ∈ B ¬ φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → ¬ φ
Assertion r2exlem ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ

Proof

Step Hyp Ref Expression
1 r2exlem.1 ⊢ ∀ x ∈ A ∀ y ∈ B ¬ φ ↔ ∀ x ∀ y x ∈ A ∧ y ∈ B → ¬ φ
2 exnal ⊢ ∃ x ¬ ∀ y x ∈ A ∧ y ∈ B → ¬ φ ↔ ¬ ∀ x ∀ y x ∈ A ∧ y ∈ B → ¬ φ
3 2 1 xchbinxr ⊢ ∃ x ¬ ∀ y x ∈ A ∧ y ∈ B → ¬ φ ↔ ¬ ∀ x ∈ A ∀ y ∈ B ¬ φ
4 exnalimn ⊢ ∃ y x ∈ A ∧ y ∈ B ∧ φ ↔ ¬ ∀ y x ∈ A ∧ y ∈ B → ¬ φ
5 4 exbii ⊢ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ ↔ ∃ x ¬ ∀ y x ∈ A ∧ y ∈ B → ¬ φ
6 ralnex2 ⊢ ∀ x ∈ A ∀ y ∈ B ¬ φ ↔ ¬ ∃ x ∈ A ∃ y ∈ B φ
7 6 con2bii ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ¬ ∀ x ∈ A ∀ y ∈ B ¬ φ
8 3 5 7 3bitr4ri ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ x ∃ y x ∈ A ∧ y ∈ B ∧ φ