Theorem prelpw

Description: An unordered pair of two sets is a member of the powerclass of a class if and only if the two sets are members of that class. (Contributed by AV, 8-Jan-2020)

	Ref	Expression
Assertion	prelpw	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ↔ { 𝐴 , 𝐵 } ∈ 𝒫 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		prssg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ↔ { 𝐴 , 𝐵 } ⊆ 𝐶 ) )
2		prex	⊢ { 𝐴 , 𝐵 } ∈ V
3	2	elpw	⊢ ( { 𝐴 , 𝐵 } ∈ 𝒫 𝐶 ↔ { 𝐴 , 𝐵 } ⊆ 𝐶 )
4	1 3	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ↔ { 𝐴 , 𝐵 } ∈ 𝒫 𝐶 ) )