Theorem tpossym

Description: Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	tpossym	$$⊢FFn\left(A\times A\right)\to \left(tposF=F\leftrightarrow \forall x\in A\forall y\in AxFy=yFx\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposfn	$$⊢FFn\left(A\times A\right)\to tposFFn\left(A\times A\right)$$
2		eqfnov2	$$⊢\left(tposFFn\left(A\times A\right)\wedge FFn\left(A\times A\right)\right)\to \left(tposF=F\leftrightarrow \forall x\in A\forall y\in AxtposFy=xFy\right)$$
3	1 2	mpancom	$$⊢FFn\left(A\times A\right)\to \left(tposF=F\leftrightarrow \forall x\in A\forall y\in AxtposFy=xFy\right)$$
4		eqcom	$$⊢xtposFy=xFy\leftrightarrow xFy=xtposFy$$
5		ovtpos	$$⊢xtposFy=yFx$$
6	5	eqeq2i	$$⊢xFy=xtposFy\leftrightarrow xFy=yFx$$
7	4 6	bitri	$$⊢xtposFy=xFy\leftrightarrow xFy=yFx$$
8	7	2ralbii	$$⊢\forall x\in A\forall y\in AxtposFy=xFy\leftrightarrow \forall x\in A\forall y\in AxFy=yFx$$
9	3 8	bitrdi	$$⊢FFn\left(A\times A\right)\to \left(tposF=F\leftrightarrow \forall x\in A\forall y\in AxFy=yFx\right)$$