Description: Obsolete version of ralab2 as of 1-Dec-2023. (Contributed by Mario Carneiro, 3-Sep-2015) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ralab2.1 | |
|
Assertion | ralab2OLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralab2.1 | |
|
2 | df-ral | |
|
3 | nfsab1 | |
|
4 | nfv | |
|
5 | 3 4 | nfim | |
6 | nfv | |
|
7 | eleq1w | |
|
8 | abid | |
|
9 | 7 8 | bitrdi | |
10 | 9 1 | imbi12d | |
11 | 5 6 10 | cbvalv1 | |
12 | 2 11 | bitri | |