dfoprab4f

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 20-Dec-2008) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	dfoprab4f.x	$⊢ Ⅎ x φ$
	dfoprab4f.y	$⊢ Ⅎ y φ$
	dfoprab4f.1	$⊢ w = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
Assertion	dfoprab4f	$⊢ \{⟨w, z⟩ \| (w \in (A \times B) \land φ)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		dfoprab4f.x	$⊢ Ⅎ x φ$
2		dfoprab4f.y	$⊢ Ⅎ y φ$
3		dfoprab4f.1	$⊢ w = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
4		nfv	$⊢ Ⅎ x w = ⟨t, u⟩$
5		nfs1v	$⊢ Ⅎ x [t/ x] [u/ y] ψ$
6	1 5	nfbi	$⊢ Ⅎ x (φ \leftrightarrow [t/ x] [u/ y] ψ)$
7	4 6	nfim	$⊢ Ⅎ x (w = ⟨t, u⟩ \to (φ \leftrightarrow [t/ x] [u/ y] ψ))$
8		opeq1	$⊢ x = t \to ⟨x, u⟩ = ⟨t, u⟩$
9	8	eqeq2d	$⊢ x = t \to (w = ⟨x, u⟩ \leftrightarrow w = ⟨t, u⟩)$
10		sbequ12	$⊢ x = t \to ([u/ y] ψ \leftrightarrow [t/ x] [u/ y] ψ)$
11	10	bibi2d	$⊢ x = t \to ((φ \leftrightarrow [u/ y] ψ) \leftrightarrow (φ \leftrightarrow [t/ x] [u/ y] ψ))$
12	9 11	imbi12d	$⊢ x = t \to ((w = ⟨x, u⟩ \to (φ \leftrightarrow [u/ y] ψ)) \leftrightarrow (w = ⟨t, u⟩ \to (φ \leftrightarrow [t/ x] [u/ y] ψ)))$
13		nfv	$⊢ Ⅎ y w = ⟨x, u⟩$
14		nfs1v	$⊢ Ⅎ y [u/ y] ψ$
15	2 14	nfbi	$⊢ Ⅎ y (φ \leftrightarrow [u/ y] ψ)$
16	13 15	nfim	$⊢ Ⅎ y (w = ⟨x, u⟩ \to (φ \leftrightarrow [u/ y] ψ))$
17		opeq2	$⊢ y = u \to ⟨x, y⟩ = ⟨x, u⟩$
18	17	eqeq2d	$⊢ y = u \to (w = ⟨x, y⟩ \leftrightarrow w = ⟨x, u⟩)$
19		sbequ12	$⊢ y = u \to (ψ \leftrightarrow [u/ y] ψ)$
20	19	bibi2d	$⊢ y = u \to ((φ \leftrightarrow ψ) \leftrightarrow (φ \leftrightarrow [u/ y] ψ))$
21	18 20	imbi12d	$⊢ y = u \to ((w = ⟨x, y⟩ \to (φ \leftrightarrow ψ)) \leftrightarrow (w = ⟨x, u⟩ \to (φ \leftrightarrow [u/ y] ψ)))$
22	16 21 3	chvarfv	$⊢ w = ⟨x, u⟩ \to (φ \leftrightarrow [u/ y] ψ)$
23	7 12 22	chvarfv	$⊢ w = ⟨t, u⟩ \to (φ \leftrightarrow [t/ x] [u/ y] ψ)$
24	23	dfoprab4	$⊢ \{⟨w, z⟩ \| (w \in (A \times B) \land φ)\} = \{⟨⟨t, u⟩, z⟩ \| ((t \in A \land u \in B) \land [t/ x] [u/ y] ψ)\}$
25		nfv	$⊢ Ⅎ t ((x \in A \land y \in B) \land ψ)$
26		nfv	$⊢ Ⅎ u ((x \in A \land y \in B) \land ψ)$
27		nfv	$⊢ Ⅎ x (t \in A \land u \in B)$
28	27 5	nfan	$⊢ Ⅎ x ((t \in A \land u \in B) \land [t/ x] [u/ y] ψ)$
29		nfv	$⊢ Ⅎ y (t \in A \land u \in B)$
30	14	nfsbv	$⊢ Ⅎ y [t/ x] [u/ y] ψ$
31	29 30	nfan	$⊢ Ⅎ y ((t \in A \land u \in B) \land [t/ x] [u/ y] ψ)$
32		eleq1w	$⊢ x = t \to (x \in A \leftrightarrow t \in A)$
33		eleq1w	$⊢ y = u \to (y \in B \leftrightarrow u \in B)$
34	32 33	bi2anan9	$⊢ (x = t \land y = u) \to ((x \in A \land y \in B) \leftrightarrow (t \in A \land u \in B))$
35	19 10	sylan9bbr	$⊢ (x = t \land y = u) \to (ψ \leftrightarrow [t/ x] [u/ y] ψ)$
36	34 35	anbi12d	$⊢ (x = t \land y = u) \to (((x \in A \land y \in B) \land ψ) \leftrightarrow ((t \in A \land u \in B) \land [t/ x] [u/ y] ψ))$
37	25 26 28 31 36	cbvoprab12	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\} = \{⟨⟨t, u⟩, z⟩ \| ((t \in A \land u \in B) \land [t/ x] [u/ y] ψ)\}$
38	24 37	eqtr4i	$⊢ \{⟨w, z⟩ \| (w \in (A \times B) \land φ)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$

Metamath Proof Explorer

Theorem dfoprab4f

Proof