Home
Metamath Proof Explorer
< Previous
Next >
Related theorems
GIF version
Syntax Definition
cpr
2468
Description:
Extend class notation to include unordered pair.
Hypotheses
Ref
Expression
cA
class
A
cB
class
B
Assertion
Ref
Expression
cpr
class
{
A
,
B
}
See definition
df-pr
2471
for more information.
Colors of variables:
wff
set
class
Copyright terms:
Public domain