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

Metamath Proof Explorer

Theorem rexiunxp

Description: Write a double restricted quantification as one universal quantifier. In this version of rexxp , B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015)

		Ref	Expression
	Hypothesis	ralxp.1	$⊢ x = ⟨y, z⟩ \to (φ \leftrightarrow ψ)$
	Assertion	rexiunxp	$⊢ \exists x \in ⋃_{y \in A} (\{y\} \times B) φ \leftrightarrow \exists y \in A \exists z \in B ψ$

Proof

Step	Hyp	Ref	Expression
1		ralxp.1	$⊢ x = ⟨y, z⟩ \to (φ \leftrightarrow ψ)$
2	1	notbid	$⊢ x = ⟨y, z⟩ \to (\neg φ \leftrightarrow \neg ψ)$
3	2	raliunxp	$⊢ \forall x \in ⋃_{y \in A} (\{y\} \times B) \neg φ \leftrightarrow \forall y \in A \forall z \in B \neg ψ$
4		ralnex	$⊢ \forall z \in B \neg ψ \leftrightarrow \neg \exists z \in B ψ$
5	4	ralbii	$⊢ \forall y \in A \forall z \in B \neg ψ \leftrightarrow \forall y \in A \neg \exists z \in B ψ$
6	3 5	bitri	$⊢ \forall x \in ⋃_{y \in A} (\{y\} \times B) \neg φ \leftrightarrow \forall y \in A \neg \exists z \in B ψ$
7	6	notbii	$⊢ \neg \forall x \in ⋃_{y \in A} (\{y\} \times B) \neg φ \leftrightarrow \neg \forall y \in A \neg \exists z \in B ψ$
8		dfrex2	$⊢ \exists x \in ⋃_{y \in A} (\{y\} \times B) φ \leftrightarrow \neg \forall x \in ⋃_{y \in A} (\{y\} \times B) \neg φ$
9		dfrex2	$⊢ \exists y \in A \exists z \in B ψ \leftrightarrow \neg \forall y \in A \neg \exists z \in B ψ$
10	7 8 9	3bitr4i	$⊢ \exists x \in ⋃_{y \in A} (\{y\} \times B) φ \leftrightarrow \exists y \in A \exists z \in B ψ$