brimg

Description: Binary relation form of the Img function. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

	Ref	Expression
Hypotheses	brimg.1	$⊢ A \in V$
	brimg.2	$⊢ B \in V$
	brimg.3	$⊢ C \in V$
Assertion	brimg	$⊢ ⟨A, B⟩ 𝖨𝗆𝗀 C \leftrightarrow C = A [B]$

Proof

Step	Hyp	Ref	Expression
1		brimg.1	$⊢ A \in V$
2		brimg.2	$⊢ B \in V$
3		brimg.3	$⊢ C \in V$
4		df-img	$⊢ 𝖨𝗆𝗀 = 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) \circ 𝖢𝖺𝗋𝗍$
5	4	breqi	$⊢ ⟨A, B⟩ 𝖨𝗆𝗀 C \leftrightarrow ⟨A, B⟩ (𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) \circ 𝖢𝖺𝗋𝗍) C$
6		opex	$⊢ ⟨A, B⟩ \in V$
7	6 3	brco	$⊢ ⟨A, B⟩ (𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) \circ 𝖢𝖺𝗋𝗍) C \leftrightarrow \exists a (⟨A, B⟩ 𝖢𝖺𝗋𝗍 a \land a 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C)$
8		vex	$⊢ a \in V$
9	1 2 8	brcart	$⊢ ⟨A, B⟩ 𝖢𝖺𝗋𝗍 a \leftrightarrow a = A \times B$
10	9	anbi1i	$⊢ (⟨A, B⟩ 𝖢𝖺𝗋𝗍 a \land a 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C) \leftrightarrow (a = A \times B \land a 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C)$
11	10	exbii	$⊢ \exists a (⟨A, B⟩ 𝖢𝖺𝗋𝗍 a \land a 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C) \leftrightarrow \exists a (a = A \times B \land a 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C)$
12	1 2	xpex	$⊢ A \times B \in V$
13		breq1	$⊢ a = A \times B \to (a 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C \leftrightarrow (A \times B) 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C)$
14	12 13	ceqsexv	$⊢ \exists a (a = A \times B \land a 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C) \leftrightarrow (A \times B) 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C$
15	7 11 14	3bitri	$⊢ ⟨A, B⟩ (𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) \circ 𝖢𝖺𝗋𝗍) C \leftrightarrow (A \times B) 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C$
16	12 3	brimage	$⊢ (A \times B) 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C \leftrightarrow C = ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) [A \times B]$
17		19.42v	$⊢ \exists a (b \in B \land (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)) \leftrightarrow (b \in B \land \exists a (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
18		anass	$⊢ ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow (p = ⟨a, b⟩ \land ((a \in A \land b \in B) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
19		an21	$⊢ ((a \in A \land b \in B) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
20	19	anbi2i	$⊢ (p = ⟨a, b⟩ \land ((a \in A \land b \in B) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)) \leftrightarrow (p = ⟨a, b⟩ \land (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)))$
21	18 20	bitri	$⊢ ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow (p = ⟨a, b⟩ \land (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)))$
22	21	2exbii	$⊢ \exists p \exists a ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow \exists p \exists a (p = ⟨a, b⟩ \land (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)))$
23		excom	$⊢ \exists p \exists a (p = ⟨a, b⟩ \land (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))) \leftrightarrow \exists a \exists p (p = ⟨a, b⟩ \land (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)))$
24		opex	$⊢ ⟨a, b⟩ \in V$
25		breq1	$⊢ p = ⟨a, b⟩ \to (p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x \leftrightarrow ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
26	25	anbi2d	$⊢ p = ⟨a, b⟩ \to ((a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
27	26	anbi2d	$⊢ p = ⟨a, b⟩ \to ((b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)) \leftrightarrow (b \in B \land (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)))$
28	24 27	ceqsexv	$⊢ \exists p (p = ⟨a, b⟩ \land (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))) \leftrightarrow (b \in B \land (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
29	28	exbii	$⊢ \exists a \exists p (p = ⟨a, b⟩ \land (b \in B \land (a \in A \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))) \leftrightarrow \exists a (b \in B \land (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
30	22 23 29	3bitri	$⊢ \exists p \exists a ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow \exists a (b \in B \land (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
31		df-br	$⊢ b A x \leftrightarrow ⟨b, x⟩ \in A$
32		risset	$⊢ ⟨b, x⟩ \in A \leftrightarrow \exists a \in A a = ⟨b, x⟩$
33		vex	$⊢ b \in V$
34	33	brresi	$⊢ a ({1^{st} ↾}_{(V \times V)}) b \leftrightarrow (a \in (V \times V) \land a 1^{st} b)$
35		df-br	$⊢ a ({1^{st} ↾}_{(V \times V)}) b \leftrightarrow ⟨a, b⟩ \in ({1^{st} ↾}_{(V \times V)})$
36	34 35	bitr3i	$⊢ (a \in (V \times V) \land a 1^{st} b) \leftrightarrow ⟨a, b⟩ \in ({1^{st} ↾}_{(V \times V)})$
37	36	anbi1i	$⊢ ((a \in (V \times V) \land a 1^{st} b) \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x) \leftrightarrow (⟨a, b⟩ \in ({1^{st} ↾}_{(V \times V)}) \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)$
38		elvv	$⊢ a \in (V \times V) \leftrightarrow \exists p \exists q a = ⟨p, q⟩$
39	38	anbi1i	$⊢ (a \in (V \times V) \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)) \leftrightarrow (\exists p \exists q a = ⟨p, q⟩ \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x))$
40		anass	$⊢ ((a \in (V \times V) \land a 1^{st} b) \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x) \leftrightarrow (a \in (V \times V) \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x))$
41		ancom	$⊢ (a = ⟨p, q⟩ \land (p = b \land q = x)) \leftrightarrow ((p = b \land q = x) \land a = ⟨p, q⟩)$
42		breq1	$⊢ a = ⟨p, q⟩ \to (a 1^{st} b \leftrightarrow ⟨p, q⟩ 1^{st} b)$
43		opeq1	$⊢ a = ⟨p, q⟩ \to ⟨a, b⟩ = ⟨⟨p, q⟩, b⟩$
44	43	breq1d	$⊢ a = ⟨p, q⟩ \to (⟨a, b⟩ (2^{nd} \circ 1^{st}) x \leftrightarrow ⟨⟨p, q⟩, b⟩ (2^{nd} \circ 1^{st}) x)$
45	42 44	anbi12d	$⊢ a = ⟨p, q⟩ \to ((a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x) \leftrightarrow (⟨p, q⟩ 1^{st} b \land ⟨⟨p, q⟩, b⟩ (2^{nd} \circ 1^{st}) x))$
46		vex	$⊢ p \in V$
47		vex	$⊢ q \in V$
48	46 47	br1steq	$⊢ ⟨p, q⟩ 1^{st} b \leftrightarrow b = p$
49		equcom	$⊢ b = p \leftrightarrow p = b$
50	48 49	bitri	$⊢ ⟨p, q⟩ 1^{st} b \leftrightarrow p = b$
51		opex	$⊢ ⟨⟨p, q⟩, b⟩ \in V$
52		vex	$⊢ x \in V$
53	51 52	brco	$⊢ ⟨⟨p, q⟩, b⟩ (2^{nd} \circ 1^{st}) x \leftrightarrow \exists a (⟨⟨p, q⟩, b⟩ 1^{st} a \land a 2^{nd} x)$
54		opex	$⊢ ⟨p, q⟩ \in V$
55	54 33	br1steq	$⊢ ⟨⟨p, q⟩, b⟩ 1^{st} a \leftrightarrow a = ⟨p, q⟩$
56	55	anbi1i	$⊢ (⟨⟨p, q⟩, b⟩ 1^{st} a \land a 2^{nd} x) \leftrightarrow (a = ⟨p, q⟩ \land a 2^{nd} x)$
57	56	exbii	$⊢ \exists a (⟨⟨p, q⟩, b⟩ 1^{st} a \land a 2^{nd} x) \leftrightarrow \exists a (a = ⟨p, q⟩ \land a 2^{nd} x)$
58	53 57	bitri	$⊢ ⟨⟨p, q⟩, b⟩ (2^{nd} \circ 1^{st}) x \leftrightarrow \exists a (a = ⟨p, q⟩ \land a 2^{nd} x)$
59		breq1	$⊢ a = ⟨p, q⟩ \to (a 2^{nd} x \leftrightarrow ⟨p, q⟩ 2^{nd} x)$
60	54 59	ceqsexv	$⊢ \exists a (a = ⟨p, q⟩ \land a 2^{nd} x) \leftrightarrow ⟨p, q⟩ 2^{nd} x$
61	46 47	br2ndeq	$⊢ ⟨p, q⟩ 2^{nd} x \leftrightarrow x = q$
62	60 61	bitri	$⊢ \exists a (a = ⟨p, q⟩ \land a 2^{nd} x) \leftrightarrow x = q$
63		equcom	$⊢ x = q \leftrightarrow q = x$
64	58 62 63	3bitri	$⊢ ⟨⟨p, q⟩, b⟩ (2^{nd} \circ 1^{st}) x \leftrightarrow q = x$
65	50 64	anbi12i	$⊢ (⟨p, q⟩ 1^{st} b \land ⟨⟨p, q⟩, b⟩ (2^{nd} \circ 1^{st}) x) \leftrightarrow (p = b \land q = x)$
66	45 65	syl6bb	$⊢ a = ⟨p, q⟩ \to ((a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x) \leftrightarrow (p = b \land q = x))$
67	66	pm5.32i	$⊢ (a = ⟨p, q⟩ \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)) \leftrightarrow (a = ⟨p, q⟩ \land (p = b \land q = x))$
68		df-3an	$⊢ (p = b \land q = x \land a = ⟨p, q⟩) \leftrightarrow ((p = b \land q = x) \land a = ⟨p, q⟩)$
69	41 67 68	3bitr4i	$⊢ (a = ⟨p, q⟩ \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)) \leftrightarrow (p = b \land q = x \land a = ⟨p, q⟩)$
70	69	2exbii	$⊢ \exists p \exists q (a = ⟨p, q⟩ \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)) \leftrightarrow \exists p \exists q (p = b \land q = x \land a = ⟨p, q⟩)$
71		19.41vv	$⊢ \exists p \exists q (a = ⟨p, q⟩ \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)) \leftrightarrow (\exists p \exists q a = ⟨p, q⟩ \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x))$
72		opeq1	$⊢ p = b \to ⟨p, q⟩ = ⟨b, q⟩$
73	72	eqeq2d	$⊢ p = b \to (a = ⟨p, q⟩ \leftrightarrow a = ⟨b, q⟩)$
74		opeq2	$⊢ q = x \to ⟨b, q⟩ = ⟨b, x⟩$
75	74	eqeq2d	$⊢ q = x \to (a = ⟨b, q⟩ \leftrightarrow a = ⟨b, x⟩)$
76	33 52 73 75	ceqsex2v	$⊢ \exists p \exists q (p = b \land q = x \land a = ⟨p, q⟩) \leftrightarrow a = ⟨b, x⟩$
77	70 71 76	3bitr3ri	$⊢ a = ⟨b, x⟩ \leftrightarrow (\exists p \exists q a = ⟨p, q⟩ \land (a 1^{st} b \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x))$
78	39 40 77	3bitr4ri	$⊢ a = ⟨b, x⟩ \leftrightarrow ((a \in (V \times V) \land a 1^{st} b) \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)$
79	52	brresi	$⊢ ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x \leftrightarrow (⟨a, b⟩ \in ({1^{st} ↾}_{(V \times V)}) \land ⟨a, b⟩ (2^{nd} \circ 1^{st}) x)$
80	37 78 79	3bitr4i	$⊢ a = ⟨b, x⟩ \leftrightarrow ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x$
81	80	rexbii	$⊢ \exists a \in A a = ⟨b, x⟩ \leftrightarrow \exists a \in A ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x$
82	32 81	bitri	$⊢ ⟨b, x⟩ \in A \leftrightarrow \exists a \in A ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x$
83		df-rex	$⊢ \exists a \in A ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x \leftrightarrow \exists a (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
84	31 82 83	3bitri	$⊢ b A x \leftrightarrow \exists a (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
85	84	anbi2i	$⊢ (b \in B \land b A x) \leftrightarrow (b \in B \land \exists a (a \in A \land ⟨a, b⟩ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x))$
86	17 30 85	3bitr4ri	$⊢ (b \in B \land b A x) \leftrightarrow \exists p \exists a ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
87	86	exbii	$⊢ \exists b (b \in B \land b A x) \leftrightarrow \exists b \exists p \exists a ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
88	52	elima2	$⊢ x \in A [B] \leftrightarrow \exists b (b \in B \land b A x)$
89	52	elima2	$⊢ x \in ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) [A \times B] \leftrightarrow \exists p (p \in (A \times B) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
90		elxp	$⊢ p \in (A \times B) \leftrightarrow \exists a \exists b (p = ⟨a, b⟩ \land (a \in A \land b \in B))$
91	90	anbi1i	$⊢ (p \in (A \times B) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow (\exists a \exists b (p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
92		19.41vv	$⊢ \exists a \exists b ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow (\exists a \exists b (p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
93	91 92	bitr4i	$⊢ (p \in (A \times B) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow \exists a \exists b ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
94	93	exbii	$⊢ \exists p (p \in (A \times B) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow \exists p \exists a \exists b ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
95		exrot3	$⊢ \exists p \exists a \exists b ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow \exists a \exists b \exists p ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
96		exrot3	$⊢ \exists a \exists b \exists p ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow \exists b \exists p \exists a ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
97	95 96	bitri	$⊢ \exists p \exists a \exists b ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x) \leftrightarrow \exists b \exists p \exists a ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
98	89 94 97	3bitri	$⊢ x \in ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) [A \times B] \leftrightarrow \exists b \exists p \exists a ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \land p ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) x)$
99	87 88 98	3bitr4ri	$⊢ x \in ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) [A \times B] \leftrightarrow x \in A [B]$
100	99	eqriv	$⊢ ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) [A \times B] = A [B]$
101	100	eqeq2i	$⊢ C = ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) [A \times B] \leftrightarrow C = A [B]$
102	16 101	bitri	$⊢ (A \times B) 𝖨𝗆𝖺𝗀𝖾 ({(2^{nd} \circ 1^{st}) ↾}_{({1^{st} ↾}_{(V \times V)})}) C \leftrightarrow C = A [B]$
103	5 15 102	3bitri	$⊢ ⟨A, B⟩ 𝖨𝗆𝗀 C \leftrightarrow C = A [B]$

Metamath Proof Explorer

Theorem brimg

Proof