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

Theorem prelpwi 5452
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 5451 . 2 ((𝐴𝐶𝐵𝐶) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
21ibi 267 1 ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  𝒫 cpw 4600  {cpr 4628
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-pw 4602  df-sn 4627  df-pr 4629
This theorem is referenced by:  inelfi  9458  elss2prb  14527  isdrs2  18352  usgrexmplef  29276  cusgrexilem2  29459  cusgrfilem2  29474  umgr2v2e  29543  vdegp1bi  29555  eupth2lem3lem5  30251  unelsiga  34135  inelpisys  34155  unelldsys  34159  measxun2  34211  saluncl  46332  prelspr  47473  prpair  47488  prproropf1olem1  47490  paireqne  47498  prprelprb  47504  isgrtri  47910  stgr1  47928  lincvalpr  48335  ldepspr  48390  zlmodzxzldeplem3  48419  zlmodzxzldep  48421  ldepsnlinc  48425
  Copyright terms: Public domain W3C validator