Theorem prelpwi 5413

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  𝒫 cpw 4554  {cpr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-pw 4556  df-sn 4582  df-pr 4584

This theorem is referenced by:  inelfi  9361  elss2prb  14498  isdrs2  18321  usgrexmplef  29406  cusgrexilem2  29589  cusgrfilem2  29603  umgr2v2e  29672  vdegp1bi  29684  eupth2lem3lem5  30380  unelsiga  34392  inelpisys  34412  unelldsys  34416  measxun2  34468  saluncl  46855  prelspr  48056  prpair  48071  prproropf1olem1  48073  paireqne  48081  prprelprb  48087  isgrtri  48529  stgr1  48547  gpgprismgr4cycllem3  48683  lincvalpr  49004  ldepspr  49059  zlmodzxzldeplem3  49088  zlmodzxzldep  49090  ldepsnlinc  49094