Theorem prprsprreu

Description: There is a unique proper unordered pair over a given set V fulfilling a wff iff there is a unique unordered pair over V of size two fulfilling this wff. (Contributed by AV, 30-Apr-2023)

	Ref	Expression
Assertion	prprsprreu	⊢ ( 𝑉 ∈ 𝑊 → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) 𝜑 ↔ ∃! 𝑝 ∈ ( Pairs ‘ 𝑉 ) ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prprspr2	⊢ ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∣ ( ♯ ‘ 𝑝 ) = 2 }
2	1	reqabi	⊢ ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
3	2	a1i	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ) )
4	3	anbi1d	⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ( ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ∧ 𝜑 ) ) )
5		anass	⊢ ( ( ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑝 ) = 2 ) ∧ 𝜑 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) )
6	4 5	bitrdi	⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) )
7	6	eubidv	⊢ ( 𝑉 ∈ 𝑊 → ( ∃! 𝑝 ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) ↔ ∃! 𝑝 ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) ) )
8		df-reu	⊢ ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) 𝜑 ↔ ∃! 𝑝 ( 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) ∧ 𝜑 ) )
9		df-reu	⊢ ( ∃! 𝑝 ∈ ( Pairs ‘ 𝑉 ) ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ↔ ∃! 𝑝 ( 𝑝 ∈ ( Pairs ‘ 𝑉 ) ∧ ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) )
10	7 8 9	3bitr4g	⊢ ( 𝑉 ∈ 𝑊 → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑉 ) 𝜑 ↔ ∃! 𝑝 ∈ ( Pairs ‘ 𝑉 ) ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜑 ) ) )