Metamath Proof Explorer
Description: Theorem *14.205 in WhiteheadRussell p. 190. (Contributed by Andrew
Salmon, 11-Jul-2011)
|
|
Ref |
Expression |
|
Assertion |
iotasbc5 |
⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] 𝜓 ↔ ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ 𝜓 ) ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
sbc5 |
⊢ ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] 𝜓 ↔ ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ 𝜓 ) ) |
2 |
1
|
a1i |
⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] 𝜓 ↔ ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ 𝜓 ) ) ) |