Metamath Proof Explorer


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 rabeq2i ( 𝑝 ∈ ( 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 ∧ 𝜑 ) ) )