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 ⊢ ∃! x φ ∧ ∃! x ψ → [˙ ι x | φ / y]˙ [˙ ι x | ψ / z]˙ χ ↔ ∃ y ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ

Proof

Step Hyp Ref Expression
1 iotasbc ⊢ ∃! x φ → [˙ ι x | φ / y]˙ [˙ ι x | ψ / z]˙ χ ↔ ∃ y ∀ x φ ↔ x = y ∧ [˙ ι x | ψ / z]˙ χ
2 iotasbc ⊢ ∃! x ψ → [˙ ι x | ψ / z]˙ χ ↔ ∃ z ∀ x ψ ↔ x = z ∧ χ
3 2 anbi2d ⊢ ∃! x ψ → ∀ x φ ↔ x = y ∧ [˙ ι x | ψ / z]˙ χ ↔ ∀ x φ ↔ x = y ∧ ∃ z ∀ x ψ ↔ x = z ∧ χ
4 3anass ⊢ ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ ↔ ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ
5 4 exbii ⊢ ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ ↔ ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ
6 19.42v ⊢ ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ ↔ ∀ x φ ↔ x = y ∧ ∃ z ∀ x ψ ↔ x = z ∧ χ
7 5 6 bitr2i ⊢ ∀ x φ ↔ x = y ∧ ∃ z ∀ x ψ ↔ x = z ∧ χ ↔ ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ
8 3 7 bitrdi ⊢ ∃! x ψ → ∀ x φ ↔ x = y ∧ [˙ ι x | ψ / z]˙ χ ↔ ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ
9 8 exbidv ⊢ ∃! x ψ → ∃ y ∀ x φ ↔ x = y ∧ [˙ ι x | ψ / z]˙ χ ↔ ∃ y ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ
10 1 9 sylan9bb ⊢ ∃! x φ ∧ ∃! x ψ → [˙ ι x | φ / y]˙ [˙ ι x | ψ / z]˙ χ ↔ ∃ y ∃ z ∀ x φ ↔ x = y ∧ ∀ x ψ ↔ x = z ∧ χ