Theorem prelpwi 5394

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  𝒫 cpw 4542  {cpr 4570

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-pw 4544  df-sn 4569  df-pr 4571

This theorem is referenced by:  inelfi  9324  elss2prb  14441  isdrs2  18263  usgrexmplef  29342  cusgrexilem2  29525  cusgrfilem2  29540  umgr2v2e  29609  vdegp1bi  29621  eupth2lem3lem5  30317  unelsiga  34294  inelpisys  34314  unelldsys  34318  measxun2  34370  saluncl  46763  prelspr  47958  prpair  47973  prproropf1olem1  47975  paireqne  47983  prprelprb  47989  isgrtri  48431  stgr1  48449  gpgprismgr4cycllem3  48585  lincvalpr  48906  ldepspr  48961  zlmodzxzldeplem3  48990  zlmodzxzldep  48992  ldepsnlinc  48996