Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Function transposition
tposeqi
Next ⟩
tposex
Metamath Proof Explorer
Ascii
Unicode
Theorem
tposeqi
Description:
Equality theorem for transposition.
(Contributed by
Mario Carneiro
, 10-Sep-2015)
Ref
Expression
Hypothesis
tposeqi.1
⊢
F
=
G
Assertion
tposeqi
⊢
tpos
F
=
tpos
G
Proof
Step
Hyp
Ref
Expression
1
tposeqi.1
⊢
F
=
G
2
tposeq
⊢
F
=
G
→
tpos
F
=
tpos
G
3
1
2
ax-mp
⊢
tpos
F
=
tpos
G