Theorem reuprpr

Description: There is a unique proper unordered pair fulfilling a wff iff there are uniquely two different sets fulfilling a corresponding wff. (Contributed by AV, 30-Apr-2023)

	Ref	Expression
Hypotheses	reupr.a	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝜓 ↔ 𝜒 ) )
	reupr.x	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( 𝜓 ↔ 𝜃 ) )
Assertion	reuprpr	⊢ ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑋 ) 𝜓 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		reupr.a	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝜓 ↔ 𝜒 ) )
2		reupr.x	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( 𝜓 ↔ 𝜃 ) )
3		prprsprreu	⊢ ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑋 ) 𝜓 ↔ ∃! 𝑝 ∈ ( Pairs ‘ 𝑋 ) ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜓 ) ) )
4		fveqeq2	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
5		hashprg	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
6	5	el2v	⊢ ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 )
7	4 6	bitr4di	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( ♯ ‘ 𝑝 ) = 2 ↔ 𝑎 ≠ 𝑏 ) )
8	7 1	anbi12d	⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜓 ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝜒 ) ) )
9		fveqeq2	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 ) )
10		hashprg	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ≠ 𝑦 ↔ ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 ) )
11	10	el2v	⊢ ( 𝑥 ≠ 𝑦 ↔ ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 )
12	9 11	bitr4di	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( ( ♯ ‘ 𝑝 ) = 2 ↔ 𝑥 ≠ 𝑦 ) )
13	12 2	anbi12d	⊢ ( 𝑝 = { 𝑥 , 𝑦 } → ( ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜓 ) ↔ ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) ) )
14	8 13	reupr	⊢ ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( Pairs ‘ 𝑋 ) ( ( ♯ ‘ 𝑝 ) = 2 ∧ 𝜓 ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( ( 𝑎 ≠ 𝑏 ∧ 𝜒 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )
15		df-3an	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ↔ ( ( 𝑎 ≠ 𝑏 ∧ 𝜒 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) )
16	15	bicomi	⊢ ( ( ( 𝑎 ≠ 𝑏 ∧ 𝜒 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) )
17	16	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( ( ( 𝑎 ≠ 𝑏 ∧ 𝜒 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )
18	17	2rexbidv	⊢ ( 𝑋 ∈ 𝑉 → ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( ( 𝑎 ≠ 𝑏 ∧ 𝜒 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )
19	3 14 18	3bitrd	⊢ ( 𝑋 ∈ 𝑉 → ( ∃! 𝑝 ∈ ( Pairsproper ‘ 𝑋 ) 𝜓 ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 ≠ 𝑦 ∧ 𝜃 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )