Theorem reuprg

Description: Convert a restricted existential uniqueness over a pair to a disjunction and an implication . (Contributed by AV, 2-Apr-2023)

	Ref	Expression
Hypotheses	reuprg.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	reuprg.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion	reuprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( ( 𝜓 ∨ 𝜒 ) ∧ ( ( 𝜒 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		reuprg.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		reuprg.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
3	1 2	reuprg0	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) )
4		orddi	⊢ ( ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ↔ ( ( ( 𝜓 ∨ 𝜒 ) ∧ ( 𝜓 ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ∧ ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ 𝜒 ) ∧ ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) )
5		curryax	⊢ ( 𝜓 ∨ ( 𝜓 → 𝐴 = 𝐵 ) )
6	5	biantru	⊢ ( ( 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜓 ∨ 𝜒 ) ∧ ( 𝜓 ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) )
7	6	bicomi	⊢ ( ( ( 𝜓 ∨ 𝜒 ) ∧ ( 𝜓 ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ↔ ( 𝜓 ∨ 𝜒 ) )
8		curryax	⊢ ( 𝜒 ∨ ( 𝜒 → 𝐴 = 𝐵 ) )
9		orcom	⊢ ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ 𝜒 ) ↔ ( 𝜒 ∨ ( 𝜒 → 𝐴 = 𝐵 ) ) )
10	8 9	mpbir	⊢ ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ 𝜒 )
11	10	biantrur	⊢ ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ↔ ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ 𝜒 ) ∧ ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) )
12	11	bicomi	⊢ ( ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ 𝜒 ) ∧ ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ↔ ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) )
13		pm4.79	⊢ ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ↔ ( ( 𝜒 ∧ 𝜓 ) → 𝐴 = 𝐵 ) )
14	12 13	bitri	⊢ ( ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ 𝜒 ) ∧ ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ↔ ( ( 𝜒 ∧ 𝜓 ) → 𝐴 = 𝐵 ) )
15	7 14	anbi12i	⊢ ( ( ( ( 𝜓 ∨ 𝜒 ) ∧ ( 𝜓 ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ∧ ( ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ 𝜒 ) ∧ ( ( 𝜒 → 𝐴 = 𝐵 ) ∨ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ) ↔ ( ( 𝜓 ∨ 𝜒 ) ∧ ( ( 𝜒 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ) )
16	4 15	bitri	⊢ ( ( ( 𝜓 ∧ ( 𝜒 → 𝐴 = 𝐵 ) ) ∨ ( 𝜒 ∧ ( 𝜓 → 𝐴 = 𝐵 ) ) ) ↔ ( ( 𝜓 ∨ 𝜒 ) ∧ ( ( 𝜒 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ) )
17	3 16	bitrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( ( 𝜓 ∨ 𝜒 ) ∧ ( ( 𝜒 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ) ) )