# 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}=\left\{3,5,7\right\}\to 𝒫{A}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 pweq ${⊢}{A}=\left\{3,5,7\right\}\to 𝒫{A}=𝒫\left\{3,5,7\right\}$
2 qdass ${⊢}\left\{\varnothing ,\left\{3\right\}\right\}\cup \left\{\left\{5\right\},\left\{3,5\right\}\right\}=\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}$
3 qdassr ${⊢}\left\{\left\{7\right\},\left\{3,7\right\}\right\}\cup \left\{\left\{5,7\right\},\left\{3,5,7\right\}\right\}=\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}$
4 2 3 uneq12i ${⊢}\left(\left\{\varnothing ,\left\{3\right\}\right\}\cup \left\{\left\{5\right\},\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\},\left\{3,7\right\}\right\}\cup \left\{\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$
5 pwtp ${⊢}𝒫\left\{3,5,7\right\}=\left(\left\{\varnothing ,\left\{3\right\}\right\}\cup \left\{\left\{5\right\},\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\},\left\{3,7\right\}\right\}\cup \left\{\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$
6 df-tp ${⊢}\left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left\{\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}$
7 6 uneq2i ${⊢}\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left\{\varnothing \right\}\cup \left(\left\{\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)$
8 unass ${⊢}\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}\right)\cup \left\{\left\{7\right\}\right\}=\left\{\varnothing \right\}\cup \left(\left\{\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)$
9 7 8 eqtr4i ${⊢}\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}\right)\cup \left\{\left\{7\right\}\right\}$
10 tpass ${⊢}\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}=\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}$
11 10 uneq1i ${⊢}\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}\right)\cup \left\{\left\{7\right\}\right\}$
12 9 11 eqtr4i ${⊢}\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}$
13 unass ${⊢}\left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\right)\cup \left\{\left\{3,5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left(\left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$
14 tpass ${⊢}\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\}\right\}$
15 14 uneq1i ${⊢}\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}=\left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\right)\cup \left\{\left\{3,5,7\right\}\right\}$
16 df-tp ${⊢}\left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}=\left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}$
17 16 uneq2i ${⊢}\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left(\left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$
18 13 15 17 3eqtr4i ${⊢}\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}$
19 12 18 uneq12i ${⊢}\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$
20 un4 ${⊢}\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$
21 19 20 eqtr4i ${⊢}\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$
22 4 5 21 3eqtr4i ${⊢}𝒫\left\{3,5,7\right\}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$
23 1 22 eqtrdi ${⊢}{A}=\left\{3,5,7\right\}\to 𝒫{A}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$