This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofrfval

Description: Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014)

		Ref	Expression
	Hypotheses	offval.1	$⊢ φ \to F Fn A$
		offval.2	$⊢ φ \to G Fn B$
		offval.3	$⊢ φ \to A \in V$
		offval.4	$⊢ φ \to B \in W$
		offval.5	$⊢ A \cap B = S$
		offval.6	$⊢ (φ \land x \in A) \to F (x) = C$
		offval.7	$⊢ (φ \land x \in B) \to G (x) = D$
	Assertion	ofrfval	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in S C R D)$

Proof

Step	Hyp	Ref	Expression
1		offval.1	$⊢ φ \to F Fn A$
2		offval.2	$⊢ φ \to G Fn B$
3		offval.3	$⊢ φ \to A \in V$
4		offval.4	$⊢ φ \to B \in W$
5		offval.5	$⊢ A \cap B = S$
6		offval.6	$⊢ (φ \land x \in A) \to F (x) = C$
7		offval.7	$⊢ (φ \land x \in B) \to G (x) = D$
8	1 3	fnexd	$⊢ φ \to F \in V$
9	2 4	fnexd	$⊢ φ \to G \in V$
10	1 2 8 9 5 6 7	ofrfvalg	$⊢ φ \to (F R_{f} G \leftrightarrow \forall x \in S C R D)$