Description: A condition showing a class is single-rooted. (See funcnv ). (Contributed by NM, 26-May-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | funcnv3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfrn2 | |
|
2 | 1 | abeq2i | |
3 | 2 | biimpi | |
4 | 3 | biantrurd | |
5 | 4 | ralbiia | |
6 | funcnv | |
|
7 | df-reu | |
|
8 | vex | |
|
9 | vex | |
|
10 | 8 9 | breldm | |
11 | 10 | pm4.71ri | |
12 | 11 | eubii | |
13 | df-eu | |
|
14 | 7 12 13 | 3bitr2i | |
15 | 14 | ralbii | |
16 | 5 6 15 | 3bitr4i | |