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	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 )
	ovid.2	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) }
Assertion	ovid	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ovid.1	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ∃! 𝑧 𝜑 )
2		ovid.2	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) }
3		df-ov	⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
4	3	eqeq1i	⊢ ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 )
5	1	fnoprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) }
6	2	fneq1i	⊢ ( 𝐹 Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ↔ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } )
7	5 6	mpbir	⊢ 𝐹 Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) }
8		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ↔ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) )
9	8	biimpri	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } )
10		fnopfvb	⊢ ( ( 𝐹 Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) } ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ) )
11	7 9 10	sylancr	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ) )
12	2	eleq2i	⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } )
13		oprabidw	⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) } ↔ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) )
14	12 13	bitri	⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ↔ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝜑 ) )
15	14	baib	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ 𝐹 ↔ 𝜑 ) )
16	11 15	bitrd	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑧 ↔ 𝜑 ) )
17	4 16	bitrid	⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ 𝜑 ) )