Theorem reuss2

Description: Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005)

	Ref	Expression
Assertion	reuss2	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
2		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
3	1 2	anbi12i	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
4		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) )
5		ssel	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
6		pm3.2	⊢ ( 𝑥 ∈ 𝐵 → ( 𝜓 → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
7	6	imim2d	⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) )
8	5 7	syl6	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝐴 → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) ) )
9	8	a2d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) ) )
10	9	imp4a	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) )
11	10	alimdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) )
12	11	imp	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
13	4 12	sylan2b	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
14		euimmo	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) → ( ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
15	13 14	syl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) → ( ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
16		df-eu	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
17	16	simplbi2	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
18	15 17	syl9	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
19	18	imp32	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) → ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
20		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
21	19 20	sylibr	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )
22	3 21	sylan2b	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) → ∃! 𝑥 ∈ 𝐴 𝜑 )