Theorem reusv2

Description: Two ways to express single-valuedness of a class expression C ( y ) that is constant for those y e. B such that ph . The first antecedent ensures that the constant value belongs to the existential uniqueness domain A , and the second ensures that C ( y ) is evaluated for at least one y . (Contributed by NM, 4-Jan-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

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

Proof

Step	Hyp	Ref	Expression
1		nfrab1	⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
2		nfcv	⊢ Ⅎ 𝑧 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
3		nfv	⊢ Ⅎ 𝑧 𝐶 ∈ 𝐴
4		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐶
5	4	nfel1	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴
6		csbeq1a	⊢ ( 𝑦 = 𝑧 → 𝐶 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
7	6	eleq1d	⊢ ( 𝑦 = 𝑧 → ( 𝐶 ∈ 𝐴 ↔ ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ) )
8	1 2 3 5 7	cbvralfw	⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝐶 ∈ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 )
9		rabid	⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
10	9	imbi1i	⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝐶 ∈ 𝐴 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐶 ∈ 𝐴 ) )
11		impexp	⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐶 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝐶 ∈ 𝐴 ) ) )
12	10 11	bitri	⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝐶 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝐶 ∈ 𝐴 ) ) )
13	12	ralbii2	⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝐶 ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 ∈ 𝐴 ) )
14	8 13	bitr3i	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 ∈ 𝐴 ) )
15		rabn0	⊢ ( { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝐵 𝜑 )
16		reusv2lem5	⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ∧ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
17		nfv	⊢ Ⅎ 𝑧 𝑥 = 𝐶
18	4	nfeq2	⊢ Ⅎ 𝑦 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶
19	6	eqeq2d	⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝐶 ↔ 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
20	1 2 17 18 19	cbvrexfw	⊢ ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
21	9	anbi1i	⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∧ 𝑥 = 𝐶 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) )
22		anass	⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) )
23	21 22	bitri	⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∧ 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) )
24	23	rexbii2	⊢ ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) )
25	20 24	bitr3i	⊢ ( ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) )
26	25	reubii	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) )
27	1 2 17 18 19	cbvralfw	⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
28	9	imbi1i	⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝑥 = 𝐶 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )
29		impexp	⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝑥 = 𝐶 ) ) )
30	28 29	bitri	⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝑥 = 𝐶 ) ) )
31	30	ralbii2	⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
32	27 31	bitr3i	⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
33	32	reubii	⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
34	16 26 33	3bitr3g	⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ∧ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
35	14 15 34	syl2anbr	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )