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	⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃! 𝑥 𝜓 ) → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] [ ( ℩ 𝑥 𝜓 ) / 𝑧 ] 𝜒 ↔ ∃ 𝑦 ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑧 ) ∧ 𝜒 ) ) )