Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tx Structured version   Unicode version

Definition df-tx 17596
 Description: Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
df-tx
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-tx
StepHypRef Expression
1 ctx 17594 . 2
2 vr . . 3
3 vs . . 3
4 cvv 2958 . . 3
5 vx . . . . . 6
6 vy . . . . . 6
72cv 1652 . . . . . 6
83cv 1652 . . . . . 6
95cv 1652 . . . . . . 7
106cv 1652 . . . . . . 7
119, 10cxp 4878 . . . . . 6
125, 6, 7, 8, 11cmpt2 6085 . . . . 5
1312crn 4881 . . . 4
14 ctg 13667 . . . 4
1513, 14cfv 5456 . . 3
162, 3, 4, 4, 15cmpt2 6085 . 2
171, 16wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  txval  17598
 Copyright terms: Public domain W3C validator