Theorem prelpwi 5430

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  𝒫 cpw 4563  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-pw 4565  df-sn 4591  df-pr 4593

This theorem is referenced by:  inelfi  9379  elss2prb  14527  isdrs2  18363  usgrexmplef  29587  cusgrexilem2  29770  cusgrfilem2  29784  umgr2v2e  29853  vdegp1bi  29865  eupth2lem3lem5  30561  unelsiga  34502  inelpisys  34522  unelldsys  34526  measxun2  34578  saluncl  47011  prelspr  48212  prpair  48227  prproropf1olem1  48229  paireqne  48237  prprelprb  48243  isgrtri  48685  stgr1  48703  gpgprismgr4cycllem3  48839  lincvalpr  49175  ldepspr  49230  zlmodzxzldeplem3  49259  zlmodzxzldep  49261  ldepsnlinc  49265