dffunALTV3

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV3 . Reproduction of dffun2 . For the X axis and the Y axis you can convert the right side to ( A. x1 A. y1 A. y2 ( ( x1 f y1 /\ x1 f y2 ) -> y1 = y2 ) /\ Rel F ) . (Contributed by NM, 29-Dec-1996)

		Ref	Expression
	Assertion	dffunALTV3	⊢ ( FunALTV 𝐹 ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ Rel 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		dffunALTV2	⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) )
2		cossssid3	⊢ ( ≀ 𝐹 ⊆ I ↔ ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) )
3	2	anbi1i	⊢ ( ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ Rel 𝐹 ) )
4	1 3	bitri	⊢ ( FunALTV 𝐹 ↔ ( ∀ 𝑢 ∀ 𝑥 ∀ 𝑦 ( ( 𝑢 𝐹 𝑥 ∧ 𝑢 𝐹 𝑦 ) → 𝑥 = 𝑦 ) ∧ Rel 𝐹 ) )

Metamath Proof Explorer

Theorem dffunALTV3

Proof