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

Theorem prelpwi 5446
Description: If two sets are members of a class, then the unordered pair of those two sets is a member of the powerclass of that class. (Contributed by Thierry Arnoux, 10-Mar-2017.) (Proof shortened by AV, 23-Oct-2021.)
Assertion
Ref Expression
prelpwi ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)

Proof of Theorem prelpwi
StepHypRef Expression
1 prelpw 5445 . 2 ((𝐴𝐶𝐵𝐶) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
21ibi 266 1 ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wcel 2104  𝒫 cpw 4601  {cpr 4629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-pw 4603  df-sn 4628  df-pr 4630
This theorem is referenced by:  inelfi  9415  elss2prb  14452  isdrs2  18263  usgrexmplef  28783  cusgrexilem2  28966  cusgrfilem2  28980  umgr2v2e  29049  vdegp1bi  29061  eupth2lem3lem5  29752  unelsiga  33430  inelpisys  33450  unelldsys  33454  measxun2  33506  saluncl  45331  prelspr  46452  prpair  46467  prproropf1olem1  46469  paireqne  46477  prprelprb  46483  lincvalpr  47186  ldepspr  47241  zlmodzxzldeplem3  47270  zlmodzxzldep  47272  ldepsnlinc  47276
  Copyright terms: Public domain W3C validator