Metamath Proof Explorer

Theorem iota4an

Description: Theorem *14.23 in WhiteheadRussell p. 191. (Contributed by Andrew Salmon, 12-Jul-2011)

Ref Expression
Assertion iota4an ⊢ ∃! x φ ∧ ψ → [˙ ι x | φ ∧ ψ / x]˙ φ

Proof

Step Hyp Ref Expression
1 iota4 ⊢ ∃! x φ ∧ ψ → [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ
2 iotaex ⊢ ι x | φ ∧ ψ ∈ V
3 simpl ⊢ φ ∧ ψ → φ
4 3 sbcth ⊢ ι x | φ ∧ ψ ∈ V → [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ → φ
5 2 4 ax-mp ⊢ [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ → φ
6 sbcimg ⊢ ι x | φ ∧ ψ ∈ V → [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ → φ ↔ [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ → [˙ ι x | φ ∧ ψ / x]˙ φ
7 2 6 ax-mp ⊢ [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ → φ ↔ [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ → [˙ ι x | φ ∧ ψ / x]˙ φ
8 5 7 mpbi ⊢ [˙ ι x | φ ∧ ψ / x]˙ φ ∧ ψ → [˙ ι x | φ ∧ ψ / x]˙ φ
9 1 8 syl ⊢ ∃! x φ ∧ ψ → [˙ ι x | φ ∧ ψ / x]˙ φ