Theorem prelpwi 5399

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

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

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-pw 4543  df-sn 4568  df-pr 4570

This theorem is referenced by:  inelfi  9331  elss2prb  14450  isdrs2  18272  usgrexmplef  29328  cusgrexilem2  29511  cusgrfilem2  29525  umgr2v2e  29594  vdegp1bi  29606  eupth2lem3lem5  30302  unelsiga  34278  inelpisys  34298  unelldsys  34302  measxun2  34354  saluncl  46745  prelspr  47946  prpair  47961  prproropf1olem1  47963  paireqne  47971  prprelprb  47977  isgrtri  48419  stgr1  48437  gpgprismgr4cycllem3  48573  lincvalpr  48894  ldepspr  48949  zlmodzxzldeplem3  48978  zlmodzxzldep  48980  ldepsnlinc  48984