Theorem prelpwi 5414

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  𝒫 cpw 4556  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-pw 4558  df-sn 4585  df-pr 4587

This theorem is used by:  inelfi  9415  elss2prb  14638  isdrs2  18487  usgrexmplef  29847  cusgrexilem2  30030  cusgrfilem2  30044  umgr2v2e  30113  vdegp1bi  30125  eupth2lem3lem5  30840  unelsiga  34814  inelpisys  34835  unelldsys  34839  measxun2  34891  saluncl  47434  prelspr  48675  prpair  48690  prproropf1olem1  48692  paireqne  48700  prprelprb  48706  isgrtri  49148  stgr1  49166  gpgprismgr4cycllem3  49302  lincvalpr  49637  ldepspr  49692  zlmodzxzldeplem3  49721  zlmodzxzldep  49723  ldepsnlinc  49727