riotasvd

Description: Deduction version of riotasv . (Contributed by NM, 4-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	riotasvd.1	$⊢ φ \to D = (ι x \in A \| \forall y \in B (ψ \to x = C))$
	riotasvd.2	$⊢ φ \to D \in A$
Assertion	riotasvd	$⊢ (φ \land A \in V) \to ((y \in B \land ψ) \to D = C)$

Proof

Step	Hyp	Ref	Expression
1		riotasvd.1	$⊢ φ \to D = (ι x \in A \| \forall y \in B (ψ \to x = C))$
2		riotasvd.2	$⊢ φ \to D \in A$
3	1	adantr	$⊢ (φ \land A \in V) \to D = (ι x \in A \| \forall y \in B (ψ \to x = C))$
4	2	adantr	$⊢ (φ \land A \in V) \to D \in A$
5	3 4	eqeltrrd	$⊢ (φ \land A \in V) \to (ι x \in A \| \forall y \in B (ψ \to x = C)) \in A$
6		riotaclbgBAD	$⊢ A \in V \to (\exists! x \in A \forall y \in B (ψ \to x = C) \leftrightarrow (ι x \in A \| \forall y \in B (ψ \to x = C)) \in A)$
7	6	adantl	$⊢ (φ \land A \in V) \to (\exists! x \in A \forall y \in B (ψ \to x = C) \leftrightarrow (ι x \in A \| \forall y \in B (ψ \to x = C)) \in A)$
8	5 7	mpbird	$⊢ (φ \land A \in V) \to \exists! x \in A \forall y \in B (ψ \to x = C)$
9		riotasbc	$⊢ \exists! x \in A \forall y \in B (ψ \to x = C) \to \underset{˙}{[} (ι x \in A \| \forall y \in B (ψ \to x = C)) / x \underset{˙}{]} \forall y \in B (ψ \to x = C)$
10	8 9	syl	$⊢ (φ \land A \in V) \to \underset{˙}{[} (ι x \in A \| \forall y \in B (ψ \to x = C)) / x \underset{˙}{]} \forall y \in B (ψ \to x = C)$
11		eqeq1	$⊢ x = z \to (x = C \leftrightarrow z = C)$
12	11	imbi2d	$⊢ x = z \to ((ψ \to x = C) \leftrightarrow (ψ \to z = C))$
13	12	ralbidv	$⊢ x = z \to (\forall y \in B (ψ \to x = C) \leftrightarrow \forall y \in B (ψ \to z = C))$
14		nfra1	$⊢ Ⅎ y \forall y \in B (ψ \to x = C)$
15		nfcv	$⊢ \underline{Ⅎ} y A$
16	14 15	nfriota	$⊢ \underline{Ⅎ} y (ι x \in A \| \forall y \in B (ψ \to x = C))$
17	16	nfeq2	$⊢ Ⅎ y z = (ι x \in A \| \forall y \in B (ψ \to x = C))$
18		eqeq1	$⊢ z = (ι x \in A \| \forall y \in B (ψ \to x = C)) \to (z = C \leftrightarrow (ι x \in A \| \forall y \in B (ψ \to x = C)) = C)$
19	18	imbi2d	$⊢ z = (ι x \in A \| \forall y \in B (ψ \to x = C)) \to ((ψ \to z = C) \leftrightarrow (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C))$
20	17 19	ralbid	$⊢ z = (ι x \in A \| \forall y \in B (ψ \to x = C)) \to (\forall y \in B (ψ \to z = C) \leftrightarrow \forall y \in B (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C))$
21	13 20	sbcie2g	$⊢ (ι x \in A \| \forall y \in B (ψ \to x = C)) \in A \to (\underset{˙}{[} (ι x \in A \| \forall y \in B (ψ \to x = C)) / x \underset{˙}{]} \forall y \in B (ψ \to x = C) \leftrightarrow \forall y \in B (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C))$
22	5 21	syl	$⊢ (φ \land A \in V) \to (\underset{˙}{[} (ι x \in A \| \forall y \in B (ψ \to x = C)) / x \underset{˙}{]} \forall y \in B (ψ \to x = C) \leftrightarrow \forall y \in B (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C))$
23	10 22	mpbid	$⊢ (φ \land A \in V) \to \forall y \in B (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C)$
24		rsp	$⊢ \forall y \in B (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C) \to (y \in B \to (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C))$
25	23 24	syl	$⊢ (φ \land A \in V) \to (y \in B \to (ψ \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C))$
26	25	impd	$⊢ (φ \land A \in V) \to ((y \in B \land ψ) \to (ι x \in A \| \forall y \in B (ψ \to x = C)) = C)$
27	3	eqeq1d	$⊢ (φ \land A \in V) \to (D = C \leftrightarrow (ι x \in A \| \forall y \in B (ψ \to x = C)) = C)$
28	26 27	sylibrd	$⊢ (φ \land A \in V) \to ((y \in B \land ψ) \to D = C)$

Metamath Proof Explorer

Theorem riotasvd

Proof