Metamath Proof Explorer


Theorem 2mos

Description: Double "there exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005) (Proof shortened by Wolf Lammen, 21-May-2025)

Ref Expression
Hypothesis 2mos.1 ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → ( 𝜑𝜓 ) )
Assertion 2mos ( ∃ 𝑧𝑤𝑥𝑦 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝑦𝑧𝑤 ( ( 𝜑𝜓 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 2mos.1 ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → ( 𝜑𝜓 ) )
2 2mo ( ∃ 𝑧𝑤𝑥𝑦 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝑦𝑧𝑤 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) )
3 1 2sbievw ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑𝜓 )
4 3 anbi2i ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( 𝜑𝜓 ) )
5 4 imbi1i ( ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ( ( 𝜑𝜓 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) )
6 5 2albii ( ∀ 𝑧𝑤 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑧𝑤 ( ( 𝜑𝜓 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) )
7 6 2albii ( ∀ 𝑥𝑦𝑧𝑤 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝑦𝑧𝑤 ( ( 𝜑𝜓 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) )
8 2 7 bitri ( ∃ 𝑧𝑤𝑥𝑦 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝑦𝑧𝑤 ( ( 𝜑𝜓 ) → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) )