brapply

Description: Binary relation form of the Apply 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	brapply.1	$⊢ A \in V$
	brapply.2	$⊢ B \in V$
	brapply.3	$⊢ C \in V$
Assertion	brapply	$⊢ ⟨A, B⟩ 𝖠𝗉𝗉𝗅𝗒 C \leftrightarrow C = A (B)$

Proof

Step	Hyp	Ref	Expression
1		brapply.1	$⊢ A \in V$
2		brapply.2	$⊢ B \in V$
3		brapply.3	$⊢ C \in V$
4		snex	$⊢ \{A [\{B\}]\} \in V$
5	4	inex1	$⊢ \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \in V$
6		unieq	$⊢ x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \to ⋃ x = ⋃ (\{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
7	6	unieqd	$⊢ x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \to ⋃ ⋃ x = ⋃ ⋃ (\{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
8	7	eqeq2d	$⊢ x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \to (C = ⋃ ⋃ x \leftrightarrow C = ⋃ ⋃ (\{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌))$
9	5 8	ceqsexv	$⊢ \exists x (x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \land C = ⋃ ⋃ x) \leftrightarrow C = ⋃ ⋃ (\{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
10		df-apply	$⊢ 𝖠𝗉𝗉𝗅𝗒 = (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) \circ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)))$
11	10	breqi	$⊢ ⟨A, B⟩ 𝖠𝗉𝗉𝗅𝗒 C \leftrightarrow ⟨A, B⟩ ((𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) \circ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)))) C$
12		opex	$⊢ ⟨A, B⟩ \in V$
13	12 3	brco	$⊢ ⟨A, B⟩ ((𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) \circ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)))) C \leftrightarrow \exists x (⟨A, B⟩ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇))) x \land x (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) C)$
14		vex	$⊢ x \in V$
15	12 14	brco	$⊢ ⟨A, B⟩ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇))) x \leftrightarrow \exists y (⟨A, B⟩ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)) y \land y ((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) x)$
16		vex	$⊢ y \in V$
17	12 16	brco	$⊢ ⟨A, B⟩ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)) y \leftrightarrow \exists z (⟨A, B⟩ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y)$
18		vex	$⊢ z \in V$
19	1 2 18	brpprod3a	$⊢ ⟨A, B⟩ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \leftrightarrow \exists a \exists b (z = ⟨a, b⟩ \land A I a \land B 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b)$
20		3anrot	$⊢ (z = ⟨a, b⟩ \land A I a \land B 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \leftrightarrow (A I a \land B 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b \land z = ⟨a, b⟩)$
21		vex	$⊢ a \in V$
22	21	ideq	$⊢ A I a \leftrightarrow A = a$
23		eqcom	$⊢ A = a \leftrightarrow a = A$
24	22 23	bitri	$⊢ A I a \leftrightarrow a = A$
25		vex	$⊢ b \in V$
26	2 25	brsingle	$⊢ B 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b \leftrightarrow b = \{B\}$
27		biid	$⊢ z = ⟨a, b⟩ \leftrightarrow z = ⟨a, b⟩$
28	24 26 27	3anbi123i	$⊢ (A I a \land B 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b \land z = ⟨a, b⟩) \leftrightarrow (a = A \land b = \{B\} \land z = ⟨a, b⟩)$
29	20 28	bitri	$⊢ (z = ⟨a, b⟩ \land A I a \land B 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \leftrightarrow (a = A \land b = \{B\} \land z = ⟨a, b⟩)$
30	29	2exbii	$⊢ \exists a \exists b (z = ⟨a, b⟩ \land A I a \land B 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 b) \leftrightarrow \exists a \exists b (a = A \land b = \{B\} \land z = ⟨a, b⟩)$
31		snex	$⊢ \{B\} \in V$
32		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
33	32	eqeq2d	$⊢ a = A \to (z = ⟨a, b⟩ \leftrightarrow z = ⟨A, b⟩)$
34		opeq2	$⊢ b = \{B\} \to ⟨A, b⟩ = ⟨A, \{B\}⟩$
35	34	eqeq2d	$⊢ b = \{B\} \to (z = ⟨A, b⟩ \leftrightarrow z = ⟨A, \{B\}⟩)$
36	1 31 33 35	ceqsex2v	$⊢ \exists a \exists b (a = A \land b = \{B\} \land z = ⟨a, b⟩) \leftrightarrow z = ⟨A, \{B\}⟩$
37	19 30 36	3bitri	$⊢ ⟨A, B⟩ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \leftrightarrow z = ⟨A, \{B\}⟩$
38	37	anbi1i	$⊢ (⟨A, B⟩ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y) \leftrightarrow (z = ⟨A, \{B\}⟩ \land z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y)$
39	38	exbii	$⊢ \exists z (⟨A, B⟩ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇) z \land z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y) \leftrightarrow \exists z (z = ⟨A, \{B\}⟩ \land z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y)$
40		opex	$⊢ ⟨A, \{B\}⟩ \in V$
41		breq1	$⊢ z = ⟨A, \{B\}⟩ \to (z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y \leftrightarrow ⟨A, \{B\}⟩ (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y)$
42	40 41	ceqsexv	$⊢ \exists z (z = ⟨A, \{B\}⟩ \land z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y) \leftrightarrow ⟨A, \{B\}⟩ (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y$
43	40 16	brco	$⊢ ⟨A, \{B\}⟩ (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y \leftrightarrow \exists x (⟨A, \{B\}⟩ 𝖨𝗆𝗀 x \land x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y)$
44	1 31 14	brimg	$⊢ ⟨A, \{B\}⟩ 𝖨𝗆𝗀 x \leftrightarrow x = A [\{B\}]$
45	14 16	brsingle	$⊢ x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y \leftrightarrow y = \{x\}$
46	44 45	anbi12i	$⊢ (⟨A, \{B\}⟩ 𝖨𝗆𝗀 x \land x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y) \leftrightarrow (x = A [\{B\}] \land y = \{x\})$
47	46	exbii	$⊢ \exists x (⟨A, \{B\}⟩ 𝖨𝗆𝗀 x \land x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y) \leftrightarrow \exists x (x = A [\{B\}] \land y = \{x\})$
48	1	imaex	$⊢ A [\{B\}] \in V$
49		sneq	$⊢ x = A [\{B\}] \to \{x\} = \{A [\{B\}]\}$
50	49	eqeq2d	$⊢ x = A [\{B\}] \to (y = \{x\} \leftrightarrow y = \{A [\{B\}]\})$
51	48 50	ceqsexv	$⊢ \exists x (x = A [\{B\}] \land y = \{x\}) \leftrightarrow y = \{A [\{B\}]\}$
52	47 51	bitri	$⊢ \exists x (⟨A, \{B\}⟩ 𝖨𝗆𝗀 x \land x 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 y) \leftrightarrow y = \{A [\{B\}]\}$
53	42 43 52	3bitri	$⊢ \exists z (z = ⟨A, \{B\}⟩ \land z (𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) y) \leftrightarrow y = \{A [\{B\}]\}$
54	17 39 53	3bitri	$⊢ ⟨A, B⟩ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)) y \leftrightarrow y = \{A [\{B\}]\}$
55		eqid	$⊢ (V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V)) = (V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))$
56		brxp	$⊢ y (V \times V) x \leftrightarrow (y \in V \land x \in V)$
57	16 14 56	mpbir2an	$⊢ y (V \times V) x$
58		epel	$⊢ z E y \leftrightarrow z \in y$
59	58	anbi1ci	$⊢ (z \in 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \land z E y) \leftrightarrow (z \in y \land z \in 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
60	16	brresi	$⊢ z ({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) y \leftrightarrow (z \in 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \land z E y)$
61		elin	$⊢ z \in (y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) \leftrightarrow (z \in y \land z \in 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
62	59 60 61	3bitr4ri	$⊢ z \in (y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) \leftrightarrow z ({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) y$
63	16 14 55 57 62	brtxpsd3	$⊢ y ((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) x \leftrightarrow x = y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌$
64	54 63	anbi12i	$⊢ (⟨A, B⟩ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)) y \land y ((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) x) \leftrightarrow (y = \{A [\{B\}]\} \land x = y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
65	64	exbii	$⊢ \exists y (⟨A, B⟩ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇)) y \land y ((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) x) \leftrightarrow \exists y (y = \{A [\{B\}]\} \land x = y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
66		ineq1	$⊢ y = \{A [\{B\}]\} \to y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌$
67	66	eqeq2d	$⊢ y = \{A [\{B\}]\} \to (x = y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \leftrightarrow x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
68	4 67	ceqsexv	$⊢ \exists y (y = \{A [\{B\}]\} \land x = y \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) \leftrightarrow x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌$
69	15 65 68	3bitri	$⊢ ⟨A, B⟩ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇))) x \leftrightarrow x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌$
70	14 3	brco	$⊢ x (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) C \leftrightarrow \exists y (x 𝖡𝗂𝗀𝖼𝗎𝗉 y \land y 𝖡𝗂𝗀𝖼𝗎𝗉 C)$
71	16	brbigcup	$⊢ x 𝖡𝗂𝗀𝖼𝗎𝗉 y \leftrightarrow ⋃ x = y$
72		eqcom	$⊢ ⋃ x = y \leftrightarrow y = ⋃ x$
73	71 72	bitri	$⊢ x 𝖡𝗂𝗀𝖼𝗎𝗉 y \leftrightarrow y = ⋃ x$
74	3	brbigcup	$⊢ y 𝖡𝗂𝗀𝖼𝗎𝗉 C \leftrightarrow ⋃ y = C$
75		eqcom	$⊢ ⋃ y = C \leftrightarrow C = ⋃ y$
76	74 75	bitri	$⊢ y 𝖡𝗂𝗀𝖼𝗎𝗉 C \leftrightarrow C = ⋃ y$
77	73 76	anbi12i	$⊢ (x 𝖡𝗂𝗀𝖼𝗎𝗉 y \land y 𝖡𝗂𝗀𝖼𝗎𝗉 C) \leftrightarrow (y = ⋃ x \land C = ⋃ y)$
78	77	exbii	$⊢ \exists y (x 𝖡𝗂𝗀𝖼𝗎𝗉 y \land y 𝖡𝗂𝗀𝖼𝗎𝗉 C) \leftrightarrow \exists y (y = ⋃ x \land C = ⋃ y)$
79		vuniex	$⊢ ⋃ x \in V$
80		unieq	$⊢ y = ⋃ x \to ⋃ y = ⋃ ⋃ x$
81	80	eqeq2d	$⊢ y = ⋃ x \to (C = ⋃ y \leftrightarrow C = ⋃ ⋃ x)$
82	79 81	ceqsexv	$⊢ \exists y (y = ⋃ x \land C = ⋃ y) \leftrightarrow C = ⋃ ⋃ x$
83	70 78 82	3bitri	$⊢ x (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) C \leftrightarrow C = ⋃ ⋃ x$
84	69 83	anbi12i	$⊢ (⟨A, B⟩ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇))) x \land x (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) C) \leftrightarrow (x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \land C = ⋃ ⋃ x)$
85	84	exbii	$⊢ \exists x (⟨A, B⟩ (((V \times V) ∖ ran ((V \otimes E) ∆ (({E ↾}_{𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌}) \otimes V))) \circ ((𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 \circ 𝖨𝗆𝗀) \circ pprod (I, 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇))) x \land x (𝖡𝗂𝗀𝖼𝗎𝗉 \circ 𝖡𝗂𝗀𝖼𝗎𝗉) C) \leftrightarrow \exists x (x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \land C = ⋃ ⋃ x)$
86	11 13 85	3bitri	$⊢ ⟨A, B⟩ 𝖠𝗉𝗉𝗅𝗒 C \leftrightarrow \exists x (x = \{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 \land C = ⋃ ⋃ x)$
87		dffv5	$⊢ A (B) = ⋃ ⋃ (\{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
88	87	eqeq2i	$⊢ C = A (B) \leftrightarrow C = ⋃ ⋃ (\{A [\{B\}]\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
89	9 86 88	3bitr4i	$⊢ ⟨A, B⟩ 𝖠𝗉𝗉𝗅𝗒 C \leftrightarrow C = A (B)$

Metamath Proof Explorer

Theorem brapply

Proof