Theorem dffunsALTV4

Description: Alternate definition of the class of functions. For the X axis and the Y axis you can convert the right side to { f e. Rels | A. x1 E* y1 x1 f y1 } . (Contributed by Peter Mazsa, 31-Aug-2021)

	Ref	Expression
Assertion	dffunsALTV4	$$⊢\mathrm{FunsALTV}=\left\{f\in \mathrm{Rels}|\forall u{\exists }^{*}xufx\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dffunsALTV	$$⊢\mathrm{FunsALTV}=\left\{f\in \mathrm{Rels}|\wr f\in \mathrm{CnvRefRels}\right\}$$
2		cosselcnvrefrels4	$$⊢\wr f\in \mathrm{CnvRefRels}\leftrightarrow \left(\forall u{\exists }^{*}xufx\wedge \wr f\in \mathrm{Rels}\right)$$
3		cosselrels	$$⊢f\in \mathrm{Rels}\to \wr f\in \mathrm{Rels}$$
4	3	biantrud	$$⊢f\in \mathrm{Rels}\to \left(\forall u{\exists }^{*}xufx\leftrightarrow \left(\forall u{\exists }^{*}xufx\wedge \wr f\in \mathrm{Rels}\right)\right)$$
5	2 4	bitr4id	$$⊢f\in \mathrm{Rels}\to \left(\wr f\in \mathrm{CnvRefRels}\leftrightarrow \forall u{\exists }^{*}xufx\right)$$
6	1 5	rabimbieq	$$⊢\mathrm{FunsALTV}=\left\{f\in \mathrm{Rels}|\forall u{\exists }^{*}xufx\right\}$$