Theorem prelpwi 5376

Description: A pair of two sets belongs to the power class of a class containing those two sets. (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 5375	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ∈ 𝒫 𝐶))
2	1	ibi 267	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ∈ 𝒫 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2104  𝒫 cpw 4539  {cpr 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-pw 4541  df-sn 4566  df-pr 4568

This theorem is referenced by:  inelfi  9221  elss2prb  14246  isdrs2  18069  usgrexmplef  27671  cusgrexilem2  27854  cusgrfilem2  27868  umgr2v2e  27937  vdegp1bi  27949  eupth2lem3lem5  28641  unelsiga  32147  inelpisys  32167  unelldsys  32171  measxun2  32223  saluncl  43907  prelspr  44996  prpair  45011  prproropf1olem1  45013  paireqne  45021  prprelprb  45027  lincvalpr  45817  ldepspr  45872  zlmodzxzldeplem3  45901  zlmodzxzldep  45903  ldepsnlinc  45907