Theorem prelpwi 5193

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2051  𝒫 cpw 4417  {cpr 4438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pr 5183

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-v 3412  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-pw 4419  df-sn 4437  df-pr 4439

This theorem is referenced by:  inelfi  8676  elss2prb  13655  isdrs2  17420  usgrexmplef  26760  cusgrexilem2  26943  cusgrfilem2  26957  umgr2v2e  27026  vdegp1bi  27038  eupth2lem3lem5  27778  unelsiga  31071  unelldsys  31095  measxun2  31147  saluncl  42063  prelspr  43046  prpair  43061  prproropf1olem1  43063  paireqne  43071  prprelprb  43077  lincvalpr  43870  ldepspr  43925  zlmodzxzldeplem3  43954  zlmodzxzldep  43956  ldepsnlinc  43960