Theorem eusvobj1

Description: Specify the same object in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016)

	Ref	Expression
Hypothesis	eusvobj1.1	⊢ 𝐵 ∈ V
Assertion	eusvobj1	⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ℩ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) = ( ℩ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eusvobj1.1	⊢ 𝐵 ∈ V
2		nfeu1	⊢ Ⅎ 𝑥 ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
3	1	eusvobj2	⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
4	2 3	alrimi	⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
5		iotabi	⊢ ( ∀ 𝑥 ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ( ℩ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) = ( ℩ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
6	4 5	syl	⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ℩ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) = ( ℩ 𝑥 ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )