Theorem prelpwi 5422

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587

This theorem is used by:  inelfi  9388  elss2prb  14553  isdrs2  18394  usgrexmplef  29719  cusgrexilem2  29902  cusgrfilem2  29916  umgr2v2e  29985  vdegp1bi  29997  eupth2lem3lem5  30712  unelsiga  34644  inelpisys  34665  unelldsys  34669  measxun2  34721  saluncl  47145  prelspr  48386  prpair  48401  prproropf1olem1  48403  paireqne  48411  prprelprb  48417  isgrtri  48859  stgr1  48877  gpgprismgr4cycllem3  49013  lincvalpr  49348  ldepspr  49403  zlmodzxzldeplem3  49432  zlmodzxzldep  49434  ldepsnlinc  49438