This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃! 𝑥 ∈ { 𝐴 , 𝐵 } 𝜑 ↔ ( ( 𝜓 ∨ 𝜒 ) ∧ ( ( 𝜒 ∧ 𝜓 ) → 𝐴 = 𝐵 ) ) ) )