Theorem prelpwi 5415

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 5414	. 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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-pw 4559  df-sn 4585  df-pr 4587

This theorem is used by:  inelfi  9403  elss2prb  14626  isdrs2  18473  usgrexmplef  29833  cusgrexilem2  30016  cusgrfilem2  30030  umgr2v2e  30099  vdegp1bi  30111  eupth2lem3lem5  30826  unelsiga  34759  inelpisys  34780  unelldsys  34784  measxun2  34836  saluncl  47296  prelspr  48537  prpair  48552  prproropf1olem1  48554  paireqne  48562  prprelprb  48568  isgrtri  49010  stgr1  49028  gpgprismgr4cycllem3  49164  lincvalpr  49499  ldepspr  49554  zlmodzxzldeplem3  49583  zlmodzxzldep  49585  ldepsnlinc  49589