Theorem prelpwi 5409

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 5408	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
2	1	ibi 266	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  𝒫 cpw 4565  {cpr 4593

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-pw 4567  df-sn 4592  df-pr 4594

This theorem is referenced by:  inelfi  9363  elss2prb  14398  isdrs2  18209  usgrexmplef  28270  cusgrexilem2  28453  cusgrfilem2  28467  umgr2v2e  28536  vdegp1bi  28548  eupth2lem3lem5  29239  unelsiga  32822  inelpisys  32842  unelldsys  32846  measxun2  32898  saluncl  44678  prelspr  45798  prpair  45813  prproropf1olem1  45815  paireqne  45823  prprelprb  45829  lincvalpr  46619  ldepspr  46674  zlmodzxzldeplem3  46703  zlmodzxzldep  46705  ldepsnlinc  46709