Metamath Proof Explorer


Theorem ex-pw

Description: Example for df-pw . Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion ex-pw A = 3 5 7 𝒫 A = 3 5 7 3 5 3 7 5 7 3 5 7

Proof

Step Hyp Ref Expression
1 pweq A = 3 5 7 𝒫 A = 𝒫 3 5 7
2 qdass 3 5 3 5 = 3 5 3 5
3 qdassr 7 3 7 5 7 3 5 7 = 7 3 7 5 7 3 5 7
4 2 3 uneq12i 3 5 3 5 7 3 7 5 7 3 5 7 = 3 5 3 5 7 3 7 5 7 3 5 7
5 pwtp 𝒫 3 5 7 = 3 5 3 5 7 3 7 5 7 3 5 7
6 df-tp 3 5 7 = 3 5 7
7 6 uneq2i 3 5 7 = 3 5 7
8 unass 3 5 7 = 3 5 7
9 7 8 eqtr4i 3 5 7 = 3 5 7
10 tpass 3 5 = 3 5
11 10 uneq1i 3 5 7 = 3 5 7
12 9 11 eqtr4i 3 5 7 = 3 5 7
13 unass 3 5 3 7 5 7 3 5 7 = 3 5 3 7 5 7 3 5 7
14 tpass 3 5 3 7 5 7 = 3 5 3 7 5 7
15 14 uneq1i 3 5 3 7 5 7 3 5 7 = 3 5 3 7 5 7 3 5 7
16 df-tp 3 7 5 7 3 5 7 = 3 7 5 7 3 5 7
17 16 uneq2i 3 5 3 7 5 7 3 5 7 = 3 5 3 7 5 7 3 5 7
18 13 15 17 3eqtr4i 3 5 3 7 5 7 3 5 7 = 3 5 3 7 5 7 3 5 7
19 12 18 uneq12i 3 5 7 3 5 3 7 5 7 3 5 7 = 3 5 7 3 5 3 7 5 7 3 5 7
20 un4 3 5 3 5 7 3 7 5 7 3 5 7 = 3 5 7 3 5 3 7 5 7 3 5 7
21 19 20 eqtr4i 3 5 7 3 5 3 7 5 7 3 5 7 = 3 5 3 5 7 3 7 5 7 3 5 7
22 4 5 21 3eqtr4i 𝒫 3 5 7 = 3 5 7 3 5 3 7 5 7 3 5 7
23 1 22 eqtrdi A = 3 5 7 𝒫 A = 3 5 7 3 5 3 7 5 7 3 5 7