Theorem prelpwi 5365

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  𝒫 cpw 4538  {cpr 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-pw 4540  df-sn 4567  df-pr 4569

This theorem is referenced by:  inelfi  9138  elss2prb  14182  isdrs2  18005  usgrexmplef  27607  cusgrexilem2  27790  cusgrfilem2  27804  umgr2v2e  27873  vdegp1bi  27885  eupth2lem3lem5  28575  unelsiga  32081  inelpisys  32101  unelldsys  32105  measxun2  32157  saluncl  43812  prelspr  44890  prpair  44905  prproropf1olem1  44907  paireqne  44915  prprelprb  44921  lincvalpr  45711  ldepspr  45766  zlmodzxzldeplem3  45795  zlmodzxzldep  45797  ldepsnlinc  45801