Theorem prelpwi 5395

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  𝒫 cpw 4554  {cpr 4582

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-pw 4556  df-sn 4581  df-pr 4583

This theorem is referenced by:  inelfi  9321  elss2prb  14411  isdrs2  18229  usgrexmplef  29332  cusgrexilem2  29515  cusgrfilem2  29530  umgr2v2e  29599  vdegp1bi  29611  eupth2lem3lem5  30307  unelsiga  34291  inelpisys  34311  unelldsys  34315  measxun2  34367  saluncl  46557  prelspr  47728  prpair  47743  prproropf1olem1  47745  paireqne  47753  prprelprb  47759  isgrtri  48185  stgr1  48203  gpgprismgr4cycllem3  48339  lincvalpr  48660  ldepspr  48715  zlmodzxzldeplem3  48744  zlmodzxzldep  48746  ldepsnlinc  48750