Metamath Proof Explorer


Theorem tpossym

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

Ref Expression
Assertion tpossym F Fn A × A tpos F = F x A y A x F y = y F x

Proof

Step Hyp Ref Expression
1 tposfn F Fn A × A tpos F Fn A × A
2 eqfnov2 tpos F Fn A × A F Fn A × A tpos F = F x A y A x tpos F y = x F y
3 1 2 mpancom F Fn A × A tpos F = F x A y A x tpos F y = x F y
4 eqcom x tpos F y = x F y 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 x F y = y F x
7 4 6 bitri x tpos F y = x F y x F y = y F x
8 7 2ralbii x A y A x tpos F y = x F y x A y A x F y = y F x
9 3 8 bitrdi F Fn A × A tpos F = F x A y A x F y = y F x