Theorem prelpwi 5388

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  𝒫 cpw 4550  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-pw 4552  df-sn 4577  df-pr 4579

This theorem is referenced by:  inelfi  9302  elss2prb  14392  isdrs2  18209  usgrexmplef  29235  cusgrexilem2  29418  cusgrfilem2  29433  umgr2v2e  29502  vdegp1bi  29514  eupth2lem3lem5  30207  unelsiga  34142  inelpisys  34162  unelldsys  34166  measxun2  34218  saluncl  46354  prelspr  47516  prpair  47531  prproropf1olem1  47533  paireqne  47541  prprelprb  47547  isgrtri  47973  stgr1  47991  gpgprismgr4cycllem3  48127  lincvalpr  48449  ldepspr  48504  zlmodzxzldeplem3  48533  zlmodzxzldep  48535  ldepsnlinc  48539