Description: Version of disjprg with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 26-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | disjprgw.1 | |
|
disjprgw.2 | |
||
Assertion | disjprgw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjprgw.1 | |
|
2 | disjprgw.2 | |
|
3 | eqeq1 | |
|
4 | nfcv | |
|
5 | nfcv | |
|
6 | 4 5 1 | csbhypf | |
7 | 6 | ineq1d | |
8 | 7 | eqeq1d | |
9 | 3 8 | orbi12d | |
10 | 9 | ralbidv | |
11 | eqeq1 | |
|
12 | nfcv | |
|
13 | nfcv | |
|
14 | 12 13 2 | csbhypf | |
15 | 14 | ineq1d | |
16 | 15 | eqeq1d | |
17 | 11 16 | orbi12d | |
18 | 17 | ralbidv | |
19 | 10 18 | ralprg | |
20 | 19 | 3adant3 | |
21 | id | |
|
22 | 21 | eqcomd | |
23 | 22 | orcd | |
24 | trud | |
|
25 | 23 24 | 2thd | |
26 | eqeq2 | |
|
27 | 12 13 2 | csbhypf | |
28 | 27 | ineq2d | |
29 | 28 | eqeq1d | |
30 | 26 29 | orbi12d | |
31 | 25 30 | ralprg | |
32 | 31 | 3adant3 | |
33 | simp3 | |
|
34 | neneq | |
|
35 | biorf | |
|
36 | 33 34 35 | 3syl | |
37 | tru | |
|
38 | 37 | biantrur | |
39 | 36 38 | bitrdi | |
40 | 32 39 | bitr4d | |
41 | eqeq2 | |
|
42 | eqcom | |
|
43 | 41 42 | bitrdi | |
44 | 4 5 1 | csbhypf | |
45 | 44 | ineq2d | |
46 | incom | |
|
47 | 45 46 | eqtrdi | |
48 | 47 | eqeq1d | |
49 | 43 48 | orbi12d | |
50 | id | |
|
51 | 50 | eqcomd | |
52 | 51 | orcd | |
53 | trud | |
|
54 | 52 53 | 2thd | |
55 | 49 54 | ralprg | |
56 | 55 | 3adant3 | |
57 | 37 | biantru | |
58 | 36 57 | bitrdi | |
59 | 56 58 | bitr4d | |
60 | 40 59 | anbi12d | |
61 | 20 60 | bitrd | |
62 | disjors | |
|
63 | pm4.24 | |
|
64 | 61 62 63 | 3bitr4g | |