Metamath Proof Explorer

Theorem raliunxp

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

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

Proof

Step	Hyp	Ref	Expression
1		ralxp.1	$⊢ x = ⟨y, z⟩ \to (φ \leftrightarrow ψ)$
2		eliunxp	$⊢ x \in ⋃_{y \in A} (\{y\} \times B) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B))$
3	2	imbi1i	$⊢ (x \in ⋃_{y \in A} (\{y\} \times B) \to φ) \leftrightarrow (\exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ)$
4		19.23vv	$⊢ \forall y \forall z ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ) \leftrightarrow (\exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ)$
5	3 4	bitr4i	$⊢ (x \in ⋃_{y \in A} (\{y\} \times B) \to φ) \leftrightarrow \forall y \forall z ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ)$
6	5	albii	$⊢ \forall x (x \in ⋃_{y \in A} (\{y\} \times B) \to φ) \leftrightarrow \forall x \forall y \forall z ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ)$
7		alrot3	$⊢ \forall x \forall y \forall z ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ) \leftrightarrow \forall y \forall z \forall x ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ)$
8		impexp	$⊢ ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ) \leftrightarrow (x = ⟨y, z⟩ \to ((y \in A \land z \in B) \to φ))$
9	8	albii	$⊢ \forall x ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ) \leftrightarrow \forall x (x = ⟨y, z⟩ \to ((y \in A \land z \in B) \to φ))$
10		opex	$⊢ ⟨y, z⟩ \in V$
11	1	imbi2d	$⊢ x = ⟨y, z⟩ \to (((y \in A \land z \in B) \to φ) \leftrightarrow ((y \in A \land z \in B) \to ψ))$
12	10 11	ceqsalv	$⊢ \forall x (x = ⟨y, z⟩ \to ((y \in A \land z \in B) \to φ)) \leftrightarrow ((y \in A \land z \in B) \to ψ)$
13	9 12	bitri	$⊢ \forall x ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ) \leftrightarrow ((y \in A \land z \in B) \to ψ)$
14	13	2albii	$⊢ \forall y \forall z \forall x ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ) \leftrightarrow \forall y \forall z ((y \in A \land z \in B) \to ψ)$
15	7 14	bitri	$⊢ \forall x \forall y \forall z ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \to φ) \leftrightarrow \forall y \forall z ((y \in A \land z \in B) \to ψ)$
16	6 15	bitri	$⊢ \forall x (x \in ⋃_{y \in A} (\{y\} \times B) \to φ) \leftrightarrow \forall y \forall z ((y \in A \land z \in B) \to ψ)$
17		df-ral	$⊢ \forall x \in ⋃_{y \in A} (\{y\} \times B) φ \leftrightarrow \forall x (x \in ⋃_{y \in A} (\{y\} \times B) \to φ)$
18		r2al	$⊢ \forall y \in A \forall z \in B ψ \leftrightarrow \forall y \forall z ((y \in A \land z \in B) \to ψ)$
19	16 17 18	3bitr4i	$⊢ \forall x \in ⋃_{y \in A} (\{y\} \times B) φ \leftrightarrow \forall y \in A \forall z \in B ψ$