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 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  𝒫 cpw 4564  {cpr 4593

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-pw 4566  df-sn 4592  df-pr 4594

This theorem is used by:  inelfi  9381  elss2prb  14538  isdrs2  18379  usgrexmplef  29638  cusgrexilem2  29821  cusgrfilem2  29835  umgr2v2e  29904  vdegp1bi  29916  eupth2lem3lem5  30612  unelsiga  34547  inelpisys  34568  unelldsys  34572  measxun2  34624  saluncl  47064  prelspr  48268  prpair  48283  prproropf1olem1  48285  paireqne  48293  prprelprb  48299  isgrtri  48741  stgr1  48759  gpgprismgr4cycllem3  48895  lincvalpr  49231  ldepspr  49286  zlmodzxzldeplem3  49315  zlmodzxzldep  49317  ldepsnlinc  49321