Metamath Proof Explorer


Theorem cover2g

Description: Two ways of expressing the statement "there is a cover of A by elements of B such that for each set in the cover, ph ". Note that ph and x must be distinct. (Contributed by Jeff Madsen, 21-Jun-2010)

Ref Expression
Hypothesis cover2g.1 A = B
Assertion cover2g B C x A y B x y φ z 𝒫 B z = A y z φ

Proof

Step Hyp Ref Expression
1 cover2g.1 A = B
2 unieq b = B b = B
3 2 1 eqtr4di b = B b = A
4 rexeq b = B y b x y φ y B x y φ
5 3 4 raleqbidv b = B x b y b x y φ x A y B x y φ
6 pweq b = B 𝒫 b = 𝒫 B
7 3 eqeq2d b = B z = b z = A
8 7 anbi1d b = B z = b y z φ z = A y z φ
9 6 8 rexeqbidv b = B z 𝒫 b z = b y z φ z 𝒫 B z = A y z φ
10 vex b V
11 eqid b = b
12 10 11 cover2 x b y b x y φ z 𝒫 b z = b y z φ
13 5 9 12 vtoclbg B C x A y B x y φ z 𝒫 B z = A y z φ