Metamath Proof Explorer


Theorem eloprabgaOLD

Description: Obsolete version of eloprabga as of 15-Oct-2024. (Contributed by NM, 14-Sep-1999) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 19-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis eloprabga.1 x = A y = B z = C φ ψ
Assertion eloprabgaOLD A V B W C X A B C x y z | φ ψ

Proof

Step Hyp Ref Expression
1 eloprabga.1 x = A y = B z = C φ ψ
2 elex A V A V
3 elex B W B V
4 elex C X C V
5 opex A B C V
6 simpr A V B V C V w = A B C w = A B C
7 6 eqeq1d A V B V C V w = A B C w = x y z A B C = x y z
8 eqcom A B C = x y z x y z = A B C
9 vex x V
10 vex y V
11 vex z V
12 9 10 11 otth2 x y z = A B C x = A y = B z = C
13 8 12 bitri A B C = x y z x = A y = B z = C
14 7 13 bitrdi A V B V C V w = A B C w = x y z x = A y = B z = C
15 14 anbi1d A V B V C V w = A B C w = x y z φ x = A y = B z = C φ
16 1 pm5.32i x = A y = B z = C φ x = A y = B z = C ψ
17 15 16 bitrdi A V B V C V w = A B C w = x y z φ x = A y = B z = C ψ
18 17 3exbidv A V B V C V w = A B C x y z w = x y z φ x y z x = A y = B z = C ψ
19 df-oprab x y z | φ = w | x y z w = x y z φ
20 19 eleq2i w x y z | φ w w | x y z w = x y z φ
21 abid w w | x y z w = x y z φ x y z w = x y z φ
22 20 21 bitr2i x y z w = x y z φ w x y z | φ
23 eleq1 w = A B C w x y z | φ A B C x y z | φ
24 22 23 syl5bb w = A B C x y z w = x y z φ A B C x y z | φ
25 24 adantl A V B V C V w = A B C x y z w = x y z φ A B C x y z | φ
26 19.41vvv x y z x = A y = B z = C ψ x y z x = A y = B z = C ψ
27 elisset A V x x = A
28 elisset B V y y = B
29 elisset C V z z = C
30 27 28 29 3anim123i A V B V C V x x = A y y = B z z = C
31 eeeanv x y z x = A y = B z = C x x = A y y = B z z = C
32 30 31 sylibr A V B V C V x y z x = A y = B z = C
33 32 biantrurd A V B V C V ψ x y z x = A y = B z = C ψ
34 26 33 bitr4id A V B V C V x y z x = A y = B z = C ψ ψ
35 34 adantr A V B V C V w = A B C x y z x = A y = B z = C ψ ψ
36 18 25 35 3bitr3d A V B V C V w = A B C A B C x y z | φ ψ
37 36 expcom w = A B C A V B V C V A B C x y z | φ ψ
38 5 37 vtocle A V B V C V A B C x y z | φ ψ
39 2 3 4 38 syl3an A V B W C X A B C x y z | φ ψ