Metamath Proof Explorer

Theorem offveqb

Description: Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014) (Proof shortened by Mario Carneiro, 5-Dec-2016)

		Ref	Expression
	Hypotheses	offveq.1	$⊢ φ \to A \in V$
		offveq.2	$⊢ φ \to F Fn A$
		offveq.3	$⊢ φ \to G Fn A$
		offveq.4	$⊢ φ \to H Fn A$
		offveq.5	$⊢ (φ \land x \in A) \to F (x) = B$
		offveq.6	$⊢ (φ \land x \in A) \to G (x) = C$
	Assertion	offveqb	$⊢ φ \to (H = F R_{f} G \leftrightarrow \forall x \in A H (x) = B R C)$

Proof

Step	Hyp	Ref	Expression
1		offveq.1	$⊢ φ \to A \in V$
2		offveq.2	$⊢ φ \to F Fn A$
3		offveq.3	$⊢ φ \to G Fn A$
4		offveq.4	$⊢ φ \to H Fn A$
5		offveq.5	$⊢ (φ \land x \in A) \to F (x) = B$
6		offveq.6	$⊢ (φ \land x \in A) \to G (x) = C$
7		dffn5	$⊢ H Fn A \leftrightarrow H = (x \in A ⟼ H (x))$
8	4 7	sylib	$⊢ φ \to H = (x \in A ⟼ H (x))$
9		inidm	$⊢ A \cap A = A$
10	2 3 1 1 9 5 6	offval	$⊢ φ \to F R_{f} G = (x \in A ⟼ B R C)$
11	8 10	eqeq12d	$⊢ φ \to (H = F R_{f} G \leftrightarrow (x \in A ⟼ H (x)) = (x \in A ⟼ B R C))$
12		fvexd	$⊢ φ \to H (x) \in V$
13	12	ralrimivw	$⊢ φ \to \forall x \in A H (x) \in V$
14		mpteqb	$⊢ \forall x \in A H (x) \in V \to ((x \in A ⟼ H (x)) = (x \in A ⟼ B R C) \leftrightarrow \forall x \in A H (x) = B R C)$
15	13 14	syl	$⊢ φ \to ((x \in A ⟼ H (x)) = (x \in A ⟼ B R C) \leftrightarrow \forall x \in A H (x) = B R C)$
16	11 15	bitrd	$⊢ φ \to (H = F R_{f} G \leftrightarrow \forall x \in A H (x) = B R C)$