Theorem prelpwi 5467

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  𝒫 cpw 4622  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-pw 4624  df-sn 4649  df-pr 4651

This theorem is referenced by:  inelfi  9487  elss2prb  14537  isdrs2  18376  usgrexmplef  29294  cusgrexilem2  29477  cusgrfilem2  29492  umgr2v2e  29561  vdegp1bi  29573  eupth2lem3lem5  30264  unelsiga  34098  inelpisys  34118  unelldsys  34122  measxun2  34174  saluncl  46238  prelspr  47360  prpair  47375  prproropf1olem1  47377  paireqne  47385  prprelprb  47391  isgrtri  47794  lincvalpr  48147  ldepspr  48202  zlmodzxzldeplem3  48231  zlmodzxzldep  48233  ldepsnlinc  48237