Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | brabd.exa | |
|
brabd.exb | |
||
brabd.def | |
||
brabd.is | |
||
Assertion | brabd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brabd.exa | |
|
2 | brabd.exb | |
|
3 | brabd.def | |
|
4 | brabd.is | |
|
5 | ax-5 | |
|
6 | ax-5 | |
|
7 | nfvd | |
|
8 | nfvd | |
|
9 | 5 6 7 8 1 2 3 4 | brabd0 | |