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

Metamath Proof Explorer

Theorem iotavalb

Description: Theorem *14.202 in WhiteheadRussell p. 189. A biconditional version of iotaval . (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotavalb ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 iotaval ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
2 iotasbc ⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝑧 = 𝑦 ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) ) )
3 iotaexeu ⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ∈ V )
4 eqsbc1 ⊢ ( ( ℩ 𝑥 𝜑 ) ∈ V → ( [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝑧 = 𝑦 ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )
5 3 4 syl ⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝑧 = 𝑦 ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )
6 2 5 bitr3d ⊢ ( ∃! 𝑥 𝜑 → ( ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )
7 equequ2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
8 7 bibi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
9 8 albidv ⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
10 9 biimpac ⊢ ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
11 10 exlimiv ⊢ ( ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
12 6 11 biimtrrdi ⊢ ( ∃! 𝑥 𝜑 → ( ( ℩ 𝑥 𝜑 ) = 𝑦 → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
13 1 12 impbid2 ⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )