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

Theorem prelpwi 5305
 Description: A pair of two sets belongs to the power class of a class containing those two sets. (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 5304 . 2 ((𝐴𝐶𝐵𝐶) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
21ibi 270 1 ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  𝒫 cpw 4497  {cpr 4527 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-pr 4528 This theorem is referenced by:  inelfi  8866  elss2prb  13841  isdrs2  17541  usgrexmplef  27049  cusgrexilem2  27232  cusgrfilem2  27246  umgr2v2e  27315  vdegp1bi  27327  eupth2lem3lem5  28017  unelsiga  31503  inelpisys  31523  unelldsys  31527  measxun2  31579  saluncl  42957  prelspr  44001  prpair  44016  prproropf1olem1  44018  paireqne  44026  prprelprb  44032  lincvalpr  44825  ldepspr  44880  zlmodzxzldeplem3  44909  zlmodzxzldep  44911  ldepsnlinc  44915
 Copyright terms: Public domain W3C validator