Metamath Proof Explorer

Theorem ovid

Description: The value of an operation class abstraction. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

		Ref	Expression
	Hypotheses	ovid.1	$⊢ (x \in R \land y \in S) \to \exists! z φ$
		ovid.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
	Assertion	ovid	$⊢ (x \in R \land y \in S) \to (x F y = z \leftrightarrow φ)$

Proof

Step	Hyp	Ref	Expression
1		ovid.1	$⊢ (x \in R \land y \in S) \to \exists! z φ$
2		ovid.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
3		df-ov	$⊢ x F y = F (⟨x, y⟩)$
4	3	eqeq1i	$⊢ x F y = z \leftrightarrow F (⟨x, y⟩) = z$
5	1	fnoprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
6	2	fneq1i	$⊢ F Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\} \leftrightarrow \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
7	5 6	mpbir	$⊢ F Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
8		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in R \land y \in S)\} \leftrightarrow (x \in R \land y \in S)$
9	8	biimpri	$⊢ (x \in R \land y \in S) \to ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in R \land y \in S)\}$
10		fnopfvb	$⊢ (F Fn \{⟨x, y⟩ \| (x \in R \land y \in S)\} \land ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in R \land y \in S)\}) \to (F (⟨x, y⟩) = z \leftrightarrow ⟨⟨x, y⟩, z⟩ \in F)$
11	7 9 10	sylancr	$⊢ (x \in R \land y \in S) \to (F (⟨x, y⟩) = z \leftrightarrow ⟨⟨x, y⟩, z⟩ \in F)$
12	2	eleq2i	$⊢ ⟨⟨x, y⟩, z⟩ \in F \leftrightarrow ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
13		oprabidw	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\} \leftrightarrow ((x \in R \land y \in S) \land φ)$
14	12 13	bitri	$⊢ ⟨⟨x, y⟩, z⟩ \in F \leftrightarrow ((x \in R \land y \in S) \land φ)$
15	14	baib	$⊢ (x \in R \land y \in S) \to (⟨⟨x, y⟩, z⟩ \in F \leftrightarrow φ)$
16	11 15	bitrd	$⊢ (x \in R \land y \in S) \to (F (⟨x, y⟩) = z \leftrightarrow φ)$
17	4 16	bitrid	$⊢ (x \in R \land y \in S) \to (x F y = z \leftrightarrow φ)$