Home
Metamath Proof Explorer
< Previous
Next >
Related theorems
Unicode version
Syntax Definition
c1st
4061
Description:
Extend the definition of a class to include the first member an ordered pair function.
Assertion
Ref
Expression
c1st
See definition
df-1st
4063
for more information.
Colors of variables:
wff
set
class
Copyright terms:
Public domain