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

Metamath Proof Explorer

Theorem dffunALTV4

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV4 . This is dffun6 . For the X axis and the Y axis you can convert the right side to ( A. x1 E* y1 x1 F y1 /\ Rel F ) . (Contributed by NM, 9-Mar-1995)

		Ref	Expression
	Assertion	dffunALTV4	⊢ ( FunALTV 𝐹 ↔ ( ∀ 𝑢 ∃* 𝑥 𝑢 𝐹 𝑥 ∧ Rel 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		dffunALTV2	⊢ ( FunALTV 𝐹 ↔ ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) )
2		cossssid4	⊢ ( ≀ 𝐹 ⊆ I ↔ ∀ 𝑢 ∃* 𝑥 𝑢 𝐹 𝑥 )
3	2	anbi1i	⊢ ( ( ≀ 𝐹 ⊆ I ∧ Rel 𝐹 ) ↔ ( ∀ 𝑢 ∃* 𝑥 𝑢 𝐹 𝑥 ∧ Rel 𝐹 ) )
4	1 3	bitri	⊢ ( FunALTV 𝐹 ↔ ( ∀ 𝑢 ∃* 𝑥 𝑢 𝐹 𝑥 ∧ Rel 𝐹 ) )