tpossym

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

		Ref	Expression
	Assertion	tpossym	$⊢ F Fn (A \times A) \to (tpos F = F \leftrightarrow \forall x \in A \forall y \in A x F y = y F x)$

Step	Hyp	Ref	Expression
1		tposfn	$⊢ F Fn (A \times A) \to tpos F Fn (A \times A)$
2		eqfnov2	$⊢ (tpos F Fn (A \times A) \land F Fn (A \times A)) \to (tpos F = F \leftrightarrow \forall x \in A \forall y \in A x tpos F y = x F y)$
3	1 2	mpancom	$⊢ F Fn (A \times A) \to (tpos F = F \leftrightarrow \forall x \in A \forall y \in A x tpos F y = x F y)$
4		eqcom	$⊢ x tpos F y = x F y \leftrightarrow x F y = x tpos F y$
5		ovtpos	$⊢ x tpos F y = y F x$
6	5	eqeq2i	$⊢ x F y = x tpos F y \leftrightarrow x F y = y F x$
7	4 6	bitri	$⊢ x tpos F y = x F y \leftrightarrow x F y = y F x$
8	7	2ralbii	$⊢ \forall x \in A \forall y \in A x tpos F y = x F y \leftrightarrow \forall x \in A \forall y \in A x F y = y F x$
9	3 8	bitrdi	$⊢ F Fn (A \times A) \to (tpos F = F \leftrightarrow \forall x \in A \forall y \in A x F y = y F x)$

Metamath Proof Explorer