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

Metamath Proof Explorer

Theorem reusv1

Description: Two ways to express single-valuedness of a class expression C ( y ) . (Contributed by NM, 16-Dec-2012) (Proof shortened by Mario Carneiro, 18-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

		Ref	Expression
	Assertion	reusv1	⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 )
2	1	nfmov	⊢ Ⅎ 𝑦 ∃* 𝑥 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 )
3		rsp	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝑥 = 𝐶 ) ) )
4	3	com3l	⊢ ( 𝑦 ∈ 𝐵 → ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → 𝑥 = 𝐶 ) ) )
5	4	alrimdv	⊢ ( 𝑦 ∈ 𝐵 → ( 𝜑 → ∀ 𝑥 ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → 𝑥 = 𝐶 ) ) )
6		mo2icl	⊢ ( ∀ 𝑥 ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → 𝑥 = 𝐶 ) → ∃* 𝑥 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
7	5 6	syl6	⊢ ( 𝑦 ∈ 𝐵 → ( 𝜑 → ∃* 𝑥 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
8	2 7	rexlimi	⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
9		mormo	⊢ ( ∃* 𝑥 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
10		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ∧ ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
11	10	rbaib	⊢ ( ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
12	8 9 11	3syl	⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )