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 𝐴 = 𝐵
Assertion cover2g ( 𝐵𝐶 → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( 𝑧 = 𝐴 ∧ ∀ 𝑦𝑧 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 cover2g.1 𝐴 = 𝐵
2 unieq ( 𝑏 = 𝐵 𝑏 = 𝐵 )
3 2 1 eqtr4di ( 𝑏 = 𝐵 𝑏 = 𝐴 )
4 rexeq ( 𝑏 = 𝐵 → ( ∃ 𝑦𝑏 ( 𝑥𝑦𝜑 ) ↔ ∃ 𝑦𝐵 ( 𝑥𝑦𝜑 ) ) )
5 3 4 raleqbidv ( 𝑏 = 𝐵 → ( ∀ 𝑥 𝑏𝑦𝑏 ( 𝑥𝑦𝜑 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝜑 ) ) )
6 pweq ( 𝑏 = 𝐵 → 𝒫 𝑏 = 𝒫 𝐵 )
7 3 eqeq2d ( 𝑏 = 𝐵 → ( 𝑧 = 𝑏 𝑧 = 𝐴 ) )
8 7 anbi1d ( 𝑏 = 𝐵 → ( ( 𝑧 = 𝑏 ∧ ∀ 𝑦𝑧 𝜑 ) ↔ ( 𝑧 = 𝐴 ∧ ∀ 𝑦𝑧 𝜑 ) ) )
9 6 8 rexeqbidv ( 𝑏 = 𝐵 → ( ∃ 𝑧 ∈ 𝒫 𝑏 ( 𝑧 = 𝑏 ∧ ∀ 𝑦𝑧 𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( 𝑧 = 𝐴 ∧ ∀ 𝑦𝑧 𝜑 ) ) )
10 vex 𝑏 ∈ V
11 eqid 𝑏 = 𝑏
12 10 11 cover2 ( ∀ 𝑥 𝑏𝑦𝑏 ( 𝑥𝑦𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝑏 ( 𝑧 = 𝑏 ∧ ∀ 𝑦𝑧 𝜑 ) )
13 5 9 12 vtoclbg ( 𝐵𝐶 → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝜑 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐵 ( 𝑧 = 𝐴 ∧ ∀ 𝑦𝑧 𝜑 ) ) )