Metamath Proof Explorer


Theorem disjprgw

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 x = A C = D
disjprgw.2 x = B C = E
Assertion disjprgw A V B V A B Disj x A B C D E =

Proof

Step Hyp Ref Expression
1 disjprgw.1 x = A C = D
2 disjprgw.2 x = B C = E
3 eqeq1 y = A y = z A = z
4 nfcv _ x A
5 nfcv _ x D
6 4 5 1 csbhypf y = A y / x C = D
7 6 ineq1d y = A y / x C z / x C = D z / x C
8 7 eqeq1d y = A y / x C z / x C = D z / x C =
9 3 8 orbi12d y = A y = z y / x C z / x C = A = z D z / x C =
10 9 ralbidv y = A z A B y = z y / x C z / x C = z A B A = z D z / x C =
11 eqeq1 y = B y = z B = z
12 nfcv _ x B
13 nfcv _ x E
14 12 13 2 csbhypf y = B y / x C = E
15 14 ineq1d y = B y / x C z / x C = E z / x C
16 15 eqeq1d y = B y / x C z / x C = E z / x C =
17 11 16 orbi12d y = B y = z y / x C z / x C = B = z E z / x C =
18 17 ralbidv y = B z A B y = z y / x C z / x C = z A B B = z E z / x C =
19 10 18 ralprg A V B V y A B z A B y = z y / x C z / x C = z A B A = z D z / x C = z A B B = z E z / x C =
20 19 3adant3 A V B V A B y A B z A B y = z y / x C z / x C = z A B A = z D z / x C = z A B B = z E z / x C =
21 id z = A z = A
22 21 eqcomd z = A A = z
23 22 orcd z = A A = z D z / x C =
24 trud z = A
25 23 24 2thd z = A A = z D z / x C =
26 eqeq2 z = B A = z A = B
27 12 13 2 csbhypf z = B z / x C = E
28 27 ineq2d z = B D z / x C = D E
29 28 eqeq1d z = B D z / x C = D E =
30 26 29 orbi12d z = B A = z D z / x C = A = B D E =
31 25 30 ralprg A V B V z A B A = z D z / x C = A = B D E =
32 31 3adant3 A V B V A B z A B A = z D z / x C = A = B D E =
33 simp3 A V B V A B A B
34 neneq A B ¬ A = B
35 biorf ¬ A = B D E = A = B D E =
36 33 34 35 3syl A V B V A B D E = A = B D E =
37 tru
38 37 biantrur A = B D E = A = B D E =
39 36 38 bitrdi A V B V A B D E = A = B D E =
40 32 39 bitr4d A V B V A B z A B A = z D z / x C = D E =
41 eqeq2 z = A B = z B = A
42 eqcom B = A A = B
43 41 42 bitrdi z = A B = z A = B
44 4 5 1 csbhypf z = A z / x C = D
45 44 ineq2d z = A E z / x C = E D
46 incom E D = D E
47 45 46 eqtrdi z = A E z / x C = D E
48 47 eqeq1d z = A E z / x C = D E =
49 43 48 orbi12d z = A B = z E z / x C = A = B D E =
50 id z = B z = B
51 50 eqcomd z = B B = z
52 51 orcd z = B B = z E z / x C =
53 trud z = B
54 52 53 2thd z = B B = z E z / x C =
55 49 54 ralprg A V B V z A B B = z E z / x C = A = B D E =
56 55 3adant3 A V B V A B z A B B = z E z / x C = A = B D E =
57 37 biantru A = B D E = A = B D E =
58 36 57 bitrdi A V B V A B D E = A = B D E =
59 56 58 bitr4d A V B V A B z A B B = z E z / x C = D E =
60 40 59 anbi12d A V B V A B z A B A = z D z / x C = z A B B = z E z / x C = D E = D E =
61 20 60 bitrd A V B V A B y A B z A B y = z y / x C z / x C = D E = D E =
62 disjors Disj x A B C y A B z A B y = z y / x C z / x C =
63 pm4.24 D E = D E = D E =
64 61 62 63 3bitr4g A V B V A B Disj x A B C D E =