Theorem prelpwi 5419

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

Step	Hyp	Ref	Expression
1		prelpw 5418	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
2	1	ibi 270	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  𝒫 cpw 4558  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-pw 4560  df-sn 4586  df-pr 4588

This theorem is referenced by:  inelfi  9366  elss2prb  14515  isdrs2  18352  usgrexmplef  29518  cusgrexilem2  29701  cusgrfilem2  29715  umgr2v2e  29784  vdegp1bi  29796  eupth2lem3lem5  30492  unelsiga  34441  inelpisys  34461  unelldsys  34465  measxun2  34517  saluncl  46889  prelspr  48090  prpair  48105  prproropf1olem1  48107  paireqne  48115  prprelprb  48121  isgrtri  48563  stgr1  48581  gpgprismgr4cycllem3  48717  lincvalpr  49049  ldepspr  49104  zlmodzxzldeplem3  49133  zlmodzxzldep  49135  ldepsnlinc  49139