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

Metamath Proof Explorer

Theorem iotasbc2

Description: Theorem *14.111 in WhiteheadRussell p. 184. (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotasbc2 ( ( ∃! 𝑥 𝜑 ∧ ∃! 𝑥 𝜓 ) → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ↔ ∃ 𝑦 ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 iotasbc ⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ) ) )
2 iotasbc ⊢ ( ∃! 𝑥 𝜓 → ( [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )
3 2 anbi2d ⊢ ( ∃! 𝑥 𝜓 → ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ) ↔ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∃ 𝑧 ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) ) )
4 3anass ⊢ ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ↔ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )
5 4 exbii ⊢ ( ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )
6 19.42v ⊢ ( ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) ↔ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∃ 𝑧 ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )
7 5 6 bitr2i ⊢ ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∃ 𝑧 ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) )
8 3 7 bitrdi ⊢ ( ∃! 𝑥 𝜓 → ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ) ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )
9 8 exbidv ⊢ ( ∃! 𝑥 𝜓 → ( ∃ 𝑦 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ) ↔ ∃ 𝑦 ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )
10 1 9 sylan9bb ⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃! 𝑥 𝜓 ) → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ↔ ∃ 𝑦 ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )