Theorem bj-1uplth

Description: The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-1uplth	⊢ ( ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ ↔ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bj-pr1eq	⊢ ( ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ → pr1 ⦅ 𝐴 ⦆ = pr1 ⦅ 𝐵 ⦆ )
2		bj-pr11val	⊢ pr1 ⦅ 𝐴 ⦆ = 𝐴
3		bj-pr11val	⊢ pr1 ⦅ 𝐵 ⦆ = 𝐵
4	1 2 3	3eqtr3g	⊢ ( ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ → 𝐴 = 𝐵 )
5		bj-1upleq	⊢ ( 𝐴 = 𝐵 → ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ )
6	4 5	impbii	⊢ ( ⦅ 𝐴 ⦆ = ⦅ 𝐵 ⦆ ↔ 𝐴 = 𝐵 )