Theorem prelpwi 5422

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  𝒫 cpw 4560  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-pw 4562  df-sn 4589  df-pr 4591

This theorem is used by:  inelfi  9447  elss2prb  14674  isdrs2  18530  usgrexmplef  29897  cusgrexilem2  30080  cusgrfilem2  30094  umgr2v2e  30163  vdegp1bi  30175  eupth2lem3lem5  30890  unelsiga  34877  inelpisys  34898  unelldsys  34902  measxun2  34954  saluncl  47600  prelspr  48841  prpair  48856  prproropf1olem1  48858  paireqne  48866  prprelprb  48872  isgrtri  49314  stgr1  49332  gpgprismgr4cycllem3  49468  lincvalpr  49861  ldepspr  49916  zlmodzxzldeplem3  49945  zlmodzxzldep  49947  ldepsnlinc  49951