# Metamath Proof Explorer

## Theorem ssenen

Description: Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion ssenen ${⊢}{A}\approx {B}\to \left\{{x}|\left({x}\subseteq {A}\wedge {x}\approx {C}\right)\right\}\approx \left\{{x}|\left({x}\subseteq {B}\wedge {x}\approx {C}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 bren ${⊢}{A}\approx {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}$
2 f1odm ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \mathrm{dom}{f}={A}$
3 vex ${⊢}{f}\in \mathrm{V}$
4 3 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
5 2 4 syl6eqelr ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {A}\in \mathrm{V}$
6 pwexg ${⊢}{A}\in \mathrm{V}\to 𝒫{A}\in \mathrm{V}$
7 inex1g ${⊢}𝒫{A}\in \mathrm{V}\to 𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\in \mathrm{V}$
8 5 6 7 3syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to 𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\in \mathrm{V}$
9 f1ofo ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}:{A}\underset{onto}{⟶}{B}$
10 forn ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \mathrm{ran}{f}={B}$
11 9 10 syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \mathrm{ran}{f}={B}$
12 3 rnex ${⊢}\mathrm{ran}{f}\in \mathrm{V}$
13 11 12 syl6eqelr ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {B}\in \mathrm{V}$
14 pwexg ${⊢}{B}\in \mathrm{V}\to 𝒫{B}\in \mathrm{V}$
15 inex1g ${⊢}𝒫{B}\in \mathrm{V}\to 𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\in \mathrm{V}$
16 13 14 15 3syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to 𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\in \mathrm{V}$
17 f1of1 ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}:{A}\underset{1-1}{⟶}{B}$
18 17 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\to {f}:{A}\underset{1-1}{⟶}{B}$
19 13 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\to {B}\in \mathrm{V}$
20 simpr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\to {y}\subseteq {A}$
21 vex ${⊢}{y}\in \mathrm{V}$
22 21 a1i ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\to {y}\in \mathrm{V}$
23 f1imaen2g ${⊢}\left(\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {B}\in \mathrm{V}\right)\wedge \left({y}\subseteq {A}\wedge {y}\in \mathrm{V}\right)\right)\to {f}\left[{y}\right]\approx {y}$
24 18 19 20 22 23 syl22anc ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\to {f}\left[{y}\right]\approx {y}$
25 entr ${⊢}\left({f}\left[{y}\right]\approx {y}\wedge {y}\approx {C}\right)\to {f}\left[{y}\right]\approx {C}$
26 24 25 sylan ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\wedge {y}\approx {C}\right)\to {f}\left[{y}\right]\approx {C}$
27 26 expl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left(\left({y}\subseteq {A}\wedge {y}\approx {C}\right)\to {f}\left[{y}\right]\approx {C}\right)$
28 imassrn ${⊢}{f}\left[{y}\right]\subseteq \mathrm{ran}{f}$
29 28 10 sseqtrid ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to {f}\left[{y}\right]\subseteq {B}$
30 9 29 syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {f}\left[{y}\right]\subseteq {B}$
31 27 30 jctild ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left(\left({y}\subseteq {A}\wedge {y}\approx {C}\right)\to \left({f}\left[{y}\right]\subseteq {B}\wedge {f}\left[{y}\right]\approx {C}\right)\right)$
32 elin ${⊢}{y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({y}\in 𝒫{A}\wedge {y}\in \left\{{x}|{x}\approx {C}\right\}\right)$
33 21 elpw ${⊢}{y}\in 𝒫{A}↔{y}\subseteq {A}$
34 breq1 ${⊢}{x}={y}\to \left({x}\approx {C}↔{y}\approx {C}\right)$
35 21 34 elab ${⊢}{y}\in \left\{{x}|{x}\approx {C}\right\}↔{y}\approx {C}$
36 33 35 anbi12i ${⊢}\left({y}\in 𝒫{A}\wedge {y}\in \left\{{x}|{x}\approx {C}\right\}\right)↔\left({y}\subseteq {A}\wedge {y}\approx {C}\right)$
37 32 36 bitri ${⊢}{y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({y}\subseteq {A}\wedge {y}\approx {C}\right)$
38 elin ${⊢}{f}\left[{y}\right]\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({f}\left[{y}\right]\in 𝒫{B}\wedge {f}\left[{y}\right]\in \left\{{x}|{x}\approx {C}\right\}\right)$
39 3 imaex ${⊢}{f}\left[{y}\right]\in \mathrm{V}$
40 39 elpw ${⊢}{f}\left[{y}\right]\in 𝒫{B}↔{f}\left[{y}\right]\subseteq {B}$
41 breq1 ${⊢}{x}={f}\left[{y}\right]\to \left({x}\approx {C}↔{f}\left[{y}\right]\approx {C}\right)$
42 39 41 elab ${⊢}{f}\left[{y}\right]\in \left\{{x}|{x}\approx {C}\right\}↔{f}\left[{y}\right]\approx {C}$
43 40 42 anbi12i ${⊢}\left({f}\left[{y}\right]\in 𝒫{B}\wedge {f}\left[{y}\right]\in \left\{{x}|{x}\approx {C}\right\}\right)↔\left({f}\left[{y}\right]\subseteq {B}\wedge {f}\left[{y}\right]\approx {C}\right)$
44 38 43 bitri ${⊢}{f}\left[{y}\right]\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({f}\left[{y}\right]\subseteq {B}\wedge {f}\left[{y}\right]\approx {C}\right)$
45 31 37 44 3imtr4g ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left({y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\to {f}\left[{y}\right]\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)$
46 f1ocnv ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$
47 f1of1 ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{f}}^{-1}:{B}\underset{1-1}{⟶}{A}$
48 f1f1orn ${⊢}{{f}}^{-1}:{B}\underset{1-1}{⟶}{A}\to {{f}}^{-1}:{B}\underset{1-1 onto}{⟶}\mathrm{ran}{{f}}^{-1}$
49 f1of1 ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}\mathrm{ran}{{f}}^{-1}\to {{f}}^{-1}:{B}\underset{1-1}{⟶}\mathrm{ran}{{f}}^{-1}$
50 47 48 49 3syl ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{f}}^{-1}:{B}\underset{1-1}{⟶}\mathrm{ran}{{f}}^{-1}$
51 vex ${⊢}{z}\in \mathrm{V}$
52 51 f1imaen ${⊢}\left({{f}}^{-1}:{B}\underset{1-1}{⟶}\mathrm{ran}{{f}}^{-1}\wedge {z}\subseteq {B}\right)\to {{f}}^{-1}\left[{z}\right]\approx {z}$
53 50 52 sylan ${⊢}\left({{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\wedge {z}\subseteq {B}\right)\to {{f}}^{-1}\left[{z}\right]\approx {z}$
54 entr ${⊢}\left({{f}}^{-1}\left[{z}\right]\approx {z}\wedge {z}\approx {C}\right)\to {{f}}^{-1}\left[{z}\right]\approx {C}$
55 53 54 sylan ${⊢}\left(\left({{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\wedge {z}\subseteq {B}\right)\wedge {z}\approx {C}\right)\to {{f}}^{-1}\left[{z}\right]\approx {C}$
56 55 expl ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to \left(\left({z}\subseteq {B}\wedge {z}\approx {C}\right)\to {{f}}^{-1}\left[{z}\right]\approx {C}\right)$
57 f1ofo ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{f}}^{-1}:{B}\underset{onto}{⟶}{A}$
58 imassrn ${⊢}{{f}}^{-1}\left[{z}\right]\subseteq \mathrm{ran}{{f}}^{-1}$
59 forn ${⊢}{{f}}^{-1}:{B}\underset{onto}{⟶}{A}\to \mathrm{ran}{{f}}^{-1}={A}$
60 58 59 sseqtrid ${⊢}{{f}}^{-1}:{B}\underset{onto}{⟶}{A}\to {{f}}^{-1}\left[{z}\right]\subseteq {A}$
61 57 60 syl ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{f}}^{-1}\left[{z}\right]\subseteq {A}$
62 56 61 jctild ${⊢}{{f}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to \left(\left({z}\subseteq {B}\wedge {z}\approx {C}\right)\to \left({{f}}^{-1}\left[{z}\right]\subseteq {A}\wedge {{f}}^{-1}\left[{z}\right]\approx {C}\right)\right)$
63 46 62 syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left(\left({z}\subseteq {B}\wedge {z}\approx {C}\right)\to \left({{f}}^{-1}\left[{z}\right]\subseteq {A}\wedge {{f}}^{-1}\left[{z}\right]\approx {C}\right)\right)$
64 elin ${⊢}{z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({z}\in 𝒫{B}\wedge {z}\in \left\{{x}|{x}\approx {C}\right\}\right)$
65 51 elpw ${⊢}{z}\in 𝒫{B}↔{z}\subseteq {B}$
66 breq1 ${⊢}{x}={z}\to \left({x}\approx {C}↔{z}\approx {C}\right)$
67 51 66 elab ${⊢}{z}\in \left\{{x}|{x}\approx {C}\right\}↔{z}\approx {C}$
68 65 67 anbi12i ${⊢}\left({z}\in 𝒫{B}\wedge {z}\in \left\{{x}|{x}\approx {C}\right\}\right)↔\left({z}\subseteq {B}\wedge {z}\approx {C}\right)$
69 64 68 bitri ${⊢}{z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({z}\subseteq {B}\wedge {z}\approx {C}\right)$
70 elin ${⊢}{{f}}^{-1}\left[{z}\right]\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({{f}}^{-1}\left[{z}\right]\in 𝒫{A}\wedge {{f}}^{-1}\left[{z}\right]\in \left\{{x}|{x}\approx {C}\right\}\right)$
71 3 cnvex ${⊢}{{f}}^{-1}\in \mathrm{V}$
72 71 imaex ${⊢}{{f}}^{-1}\left[{z}\right]\in \mathrm{V}$
73 72 elpw ${⊢}{{f}}^{-1}\left[{z}\right]\in 𝒫{A}↔{{f}}^{-1}\left[{z}\right]\subseteq {A}$
74 breq1 ${⊢}{x}={{f}}^{-1}\left[{z}\right]\to \left({x}\approx {C}↔{{f}}^{-1}\left[{z}\right]\approx {C}\right)$
75 72 74 elab ${⊢}{{f}}^{-1}\left[{z}\right]\in \left\{{x}|{x}\approx {C}\right\}↔{{f}}^{-1}\left[{z}\right]\approx {C}$
76 73 75 anbi12i ${⊢}\left({{f}}^{-1}\left[{z}\right]\in 𝒫{A}\wedge {{f}}^{-1}\left[{z}\right]\in \left\{{x}|{x}\approx {C}\right\}\right)↔\left({{f}}^{-1}\left[{z}\right]\subseteq {A}\wedge {{f}}^{-1}\left[{z}\right]\approx {C}\right)$
77 70 76 bitri ${⊢}{{f}}^{-1}\left[{z}\right]\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)↔\left({{f}}^{-1}\left[{z}\right]\subseteq {A}\wedge {{f}}^{-1}\left[{z}\right]\approx {C}\right)$
78 63 69 77 3imtr4g ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left({z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\to {{f}}^{-1}\left[{z}\right]\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)$
79 simpl ${⊢}\left({z}\in 𝒫{B}\wedge {z}\in \left\{{x}|{x}\approx {C}\right\}\right)\to {z}\in 𝒫{B}$
80 79 elpwid ${⊢}\left({z}\in 𝒫{B}\wedge {z}\in \left\{{x}|{x}\approx {C}\right\}\right)\to {z}\subseteq {B}$
81 64 80 sylbi ${⊢}{z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\to {z}\subseteq {B}$
82 imaeq2 ${⊢}{y}={{f}}^{-1}\left[{z}\right]\to {f}\left[{y}\right]={f}\left[{{f}}^{-1}\left[{z}\right]\right]$
83 f1orel ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \mathrm{Rel}{f}$
84 dfrel2 ${⊢}\mathrm{Rel}{f}↔{{{f}}^{-1}}^{-1}={f}$
85 83 84 sylib ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {{{f}}^{-1}}^{-1}={f}$
86 85 imaeq1d ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {{{f}}^{-1}}^{-1}\left[{{f}}^{-1}\left[{z}\right]\right]={f}\left[{{f}}^{-1}\left[{z}\right]\right]$
87 86 adantr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\subseteq {B}\right)\to {{{f}}^{-1}}^{-1}\left[{{f}}^{-1}\left[{z}\right]\right]={f}\left[{{f}}^{-1}\left[{z}\right]\right]$
88 46 47 syl ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to {{f}}^{-1}:{B}\underset{1-1}{⟶}{A}$
89 f1imacnv ${⊢}\left({{f}}^{-1}:{B}\underset{1-1}{⟶}{A}\wedge {z}\subseteq {B}\right)\to {{{f}}^{-1}}^{-1}\left[{{f}}^{-1}\left[{z}\right]\right]={z}$
90 88 89 sylan ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\subseteq {B}\right)\to {{{f}}^{-1}}^{-1}\left[{{f}}^{-1}\left[{z}\right]\right]={z}$
91 87 90 eqtr3d ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\subseteq {B}\right)\to {f}\left[{{f}}^{-1}\left[{z}\right]\right]={z}$
92 82 91 sylan9eqr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\subseteq {B}\right)\wedge {y}={{f}}^{-1}\left[{z}\right]\right)\to {f}\left[{y}\right]={z}$
93 92 eqcomd ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\subseteq {B}\right)\wedge {y}={{f}}^{-1}\left[{z}\right]\right)\to {z}={f}\left[{y}\right]$
94 93 ex ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\subseteq {B}\right)\to \left({y}={{f}}^{-1}\left[{z}\right]\to {z}={f}\left[{y}\right]\right)$
95 81 94 sylan2 ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)\to \left({y}={{f}}^{-1}\left[{z}\right]\to {z}={f}\left[{y}\right]\right)$
96 95 adantrl ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\wedge {z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)\right)\to \left({y}={{f}}^{-1}\left[{z}\right]\to {z}={f}\left[{y}\right]\right)$
97 simpl ${⊢}\left({y}\in 𝒫{A}\wedge {y}\in \left\{{x}|{x}\approx {C}\right\}\right)\to {y}\in 𝒫{A}$
98 97 elpwid ${⊢}\left({y}\in 𝒫{A}\wedge {y}\in \left\{{x}|{x}\approx {C}\right\}\right)\to {y}\subseteq {A}$
99 32 98 sylbi ${⊢}{y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\to {y}\subseteq {A}$
100 imaeq2 ${⊢}{z}={f}\left[{y}\right]\to {{f}}^{-1}\left[{z}\right]={{f}}^{-1}\left[{f}\left[{y}\right]\right]$
101 f1imacnv ${⊢}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {y}\subseteq {A}\right)\to {{f}}^{-1}\left[{f}\left[{y}\right]\right]={y}$
102 17 101 sylan ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\to {{f}}^{-1}\left[{f}\left[{y}\right]\right]={y}$
103 100 102 sylan9eqr ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\wedge {z}={f}\left[{y}\right]\right)\to {{f}}^{-1}\left[{z}\right]={y}$
104 103 eqcomd ${⊢}\left(\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\wedge {z}={f}\left[{y}\right]\right)\to {y}={{f}}^{-1}\left[{z}\right]$
105 104 ex ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\subseteq {A}\right)\to \left({z}={f}\left[{y}\right]\to {y}={{f}}^{-1}\left[{z}\right]\right)$
106 99 105 sylan2 ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge {y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)\to \left({z}={f}\left[{y}\right]\to {y}={{f}}^{-1}\left[{z}\right]\right)$
107 106 adantrr ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\wedge {z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)\right)\to \left({z}={f}\left[{y}\right]\to {y}={{f}}^{-1}\left[{z}\right]\right)$
108 96 107 impbid ${⊢}\left({f}:{A}\underset{1-1 onto}{⟶}{B}\wedge \left({y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\wedge {z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)\right)\to \left({y}={{f}}^{-1}\left[{z}\right]↔{z}={f}\left[{y}\right]\right)$
109 108 ex ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left(\left({y}\in \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\wedge {z}\in \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)\right)\to \left({y}={{f}}^{-1}\left[{z}\right]↔{z}={f}\left[{y}\right]\right)\right)$
110 8 16 45 78 109 en3d ${⊢}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\approx \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)$
111 110 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1 onto}{⟶}{B}\to \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\approx \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)$
112 1 111 sylbi ${⊢}{A}\approx {B}\to \left(𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}\right)\approx \left(𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}\right)$
113 df-pw ${⊢}𝒫{A}=\left\{{x}|{x}\subseteq {A}\right\}$
114 113 ineq1i ${⊢}𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}=\left\{{x}|{x}\subseteq {A}\right\}\cap \left\{{x}|{x}\approx {C}\right\}$
115 inab ${⊢}\left\{{x}|{x}\subseteq {A}\right\}\cap \left\{{x}|{x}\approx {C}\right\}=\left\{{x}|\left({x}\subseteq {A}\wedge {x}\approx {C}\right)\right\}$
116 114 115 eqtri ${⊢}𝒫{A}\cap \left\{{x}|{x}\approx {C}\right\}=\left\{{x}|\left({x}\subseteq {A}\wedge {x}\approx {C}\right)\right\}$
117 df-pw ${⊢}𝒫{B}=\left\{{x}|{x}\subseteq {B}\right\}$
118 117 ineq1i ${⊢}𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}=\left\{{x}|{x}\subseteq {B}\right\}\cap \left\{{x}|{x}\approx {C}\right\}$
119 inab ${⊢}\left\{{x}|{x}\subseteq {B}\right\}\cap \left\{{x}|{x}\approx {C}\right\}=\left\{{x}|\left({x}\subseteq {B}\wedge {x}\approx {C}\right)\right\}$
120 118 119 eqtri ${⊢}𝒫{B}\cap \left\{{x}|{x}\approx {C}\right\}=\left\{{x}|\left({x}\subseteq {B}\wedge {x}\approx {C}\right)\right\}$
121 112 116 120 3brtr3g ${⊢}{A}\approx {B}\to \left\{{x}|\left({x}\subseteq {A}\wedge {x}\approx {C}\right)\right\}\approx \left\{{x}|\left({x}\subseteq {B}\wedge {x}\approx {C}\right)\right\}$