ovmpodv2

Description: Alternate deduction version of ovmpo , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017)

Step	Hyp	Ref	Expression
1		ovmpodv2.1	$⊢ φ \to A \in C$
2		ovmpodv2.2	$⊢ (φ \land x = A) \to B \in D$
3		ovmpodv2.3	$⊢ (φ \land (x = A \land y = B)) \to R \in V$
4		ovmpodv2.4	$⊢ (φ \land (x = A \land y = B)) \to R = S$
5		eqidd	$⊢ φ \to (x \in C, y \in D ⟼ R) = (x \in C, y \in D ⟼ R)$
6	4	eqeq2d	$⊢ (φ \land (x = A \land y = B)) \to (A (x \in C, y \in D ⟼ R) B = R \leftrightarrow A (x \in C, y \in D ⟼ R) B = S)$
7	6	biimpd	$⊢ (φ \land (x = A \land y = B)) \to (A (x \in C, y \in D ⟼ R) B = R \to A (x \in C, y \in D ⟼ R) B = S)$
8		nfmpo1	$⊢ \underline{Ⅎ} x (x \in C, y \in D ⟼ R)$
9		nfcv	$⊢ \underline{Ⅎ} x A$
10		nfcv	$⊢ \underline{Ⅎ} x B$
11	9 8 10	nfov	$⊢ \underline{Ⅎ} x (A (x \in C, y \in D ⟼ R) B)$
12	11	nfeq1	$⊢ Ⅎ x A (x \in C, y \in D ⟼ R) B = S$
13		nfmpo2	$⊢ \underline{Ⅎ} y (x \in C, y \in D ⟼ R)$
14		nfcv	$⊢ \underline{Ⅎ} y A$
15		nfcv	$⊢ \underline{Ⅎ} y B$
16	14 13 15	nfov	$⊢ \underline{Ⅎ} y (A (x \in C, y \in D ⟼ R) B)$
17	16	nfeq1	$⊢ Ⅎ y A (x \in C, y \in D ⟼ R) B = S$
18	1 2 3 7 8 12 13 17	ovmpodf	$⊢ φ \to ((x \in C, y \in D ⟼ R) = (x \in C, y \in D ⟼ R) \to A (x \in C, y \in D ⟼ R) B = S)$
19	5 18	mpd	$⊢ φ \to A (x \in C, y \in D ⟼ R) B = S$
20		oveq	$⊢ F = (x \in C, y \in D ⟼ R) \to A F B = A (x \in C, y \in D ⟼ R) B$
21	20	eqeq1d	$⊢ F = (x \in C, y \in D ⟼ R) \to (A F B = S \leftrightarrow A (x \in C, y \in D ⟼ R) B = S)$
22	19 21	syl5ibrcom	$⊢ φ \to (F = (x \in C, y \in D ⟼ R) \to A F B = S)$

Metamath Proof Explorer