 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwun Structured version   Visualization version   GIF version

Theorem pwun 5248
 Description: The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by NM, 23-Nov-2003.)
Assertion
Ref Expression
pwun ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵))

Proof of Theorem pwun
StepHypRef Expression
1 pwunss 5245 . . 3 (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴𝐵)
21biantru 527 . 2 (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ↔ (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴𝐵)))
3 pwssun 5246 . 2 ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
4 eqss 3842 . 2 (𝒫 (𝐴𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵) ↔ (𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵) ∧ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴𝐵)))
52, 3, 43bitr4i 295 1 ((𝐴𝐵𝐵𝐴) ↔ 𝒫 (𝐴𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198   ∧ wa 386   ∨ wo 880   = wceq 1658   ∪ cun 3796   ⊆ wss 3798  𝒫 cpw 4378 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803  ax-sep 5005  ax-pr 5127 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-in 3805  df-ss 3812  df-pw 4380  df-sn 4398  df-pr 4400 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator