Description: There is exactly one ordered ordered pair fulfilling a wff iff there is exactly one proper pair fulfilling an equivalent wff. (Contributed by AV, 20-Mar-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prproropreud.o | |
|
prproropreud.p | |
||
prproropreud.b | |
||
prproropreud.x | |
||
prproropreud.z | |
||
Assertion | prproropreud | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prproropreud.o | |
|
2 | prproropreud.p | |
|
3 | prproropreud.b | |
|
4 | prproropreud.x | |
|
5 | prproropreud.z | |
|
6 | eqid | |
|
7 | 1 2 6 | prproropf1o | |
8 | 3 7 | syl | |
9 | sbceq1a | |
|
10 | 9 | adantl | |
11 | nfsbc1v | |
|
12 | 8 10 5 11 | reuf1odnf | |
13 | eqidd | |
|
14 | infeq1 | |
|
15 | supeq1 | |
|
16 | 14 15 | opeq12d | |
17 | 16 | adantl | |
18 | simpr | |
|
19 | opex | |
|
20 | 19 | a1i | |
21 | 13 17 18 20 | fvmptd | |
22 | 21 | sbceq1d | |
23 | 4 | sbcieg | |
24 | 20 23 | syl | |
25 | 22 24 | bitrd | |
26 | 25 | reubidva | |
27 | 12 26 | bitrd | |