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	$⊢ \forall x \in A \forall y \in B \neg φ \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to \neg φ)$
	Assertion	r2exlem	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land φ)$

Proof

Step	Hyp	Ref	Expression
1		r2exlem.1	$⊢ \forall x \in A \forall y \in B \neg φ \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to \neg φ)$
2		exnal	$⊢ \exists x \neg \forall y ((x \in A \land y \in B) \to \neg φ) \leftrightarrow \neg \forall x \forall y ((x \in A \land y \in B) \to \neg φ)$
3	2 1	xchbinxr	$⊢ \exists x \neg \forall y ((x \in A \land y \in B) \to \neg φ) \leftrightarrow \neg \forall x \in A \forall y \in B \neg φ$
4		exnalimn	$⊢ \exists y ((x \in A \land y \in B) \land φ) \leftrightarrow \neg \forall y ((x \in A \land y \in B) \to \neg φ)$
5	4	exbii	$⊢ \exists x \exists y ((x \in A \land y \in B) \land φ) \leftrightarrow \exists x \neg \forall y ((x \in A \land y \in B) \to \neg φ)$
6		ralnex2	$⊢ \forall x \in A \forall y \in B \neg φ \leftrightarrow \neg \exists x \in A \exists y \in B φ$
7	6	con2bii	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \neg \forall x \in A \forall y \in B \neg φ$
8	3 5 7	3bitr4ri	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land φ)$