Theorem reusv2 5372

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

Assertion

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

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦)   𝐵(𝑦)   𝐶(𝑦)

Proof of Theorem reusv2

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfrab1 3434	. . . 4 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑}
2		nfcv 2924	. . . 4 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
3		nfv 1947	. . . 4 ⊢ Ⅎ𝑧 𝐶 ∈ 𝐴
4		nfcsb1v 3874	. . . . 5 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶
5	4	nfel1 2940	. . . 4 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴
6		csbeq1a 3864	. . . . 5 ⊢ (𝑦 = 𝑧 → 𝐶 = ⦋𝑧 / 𝑦⦌𝐶)
7	6	eleq1d 2847	. . . 4 ⊢ (𝑦 = 𝑧 → (𝐶 ∈ 𝐴 ↔ ⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴))
8	1, 2, 3, 5, 7	cbvralfw 3304	. . 3 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴)
9		rabid 3435	. . . . . 6 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑))
10	9	imbi1i 352	. . . . 5 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴))
11		impexp 456	. . . . 5 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴)))
12	10, 11	bitri 278	. . . 4 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴)))
13	12	ralbii2 3106	. . 3 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴))
14	8, 13	bitr3i 280	. 2 ⊢ (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴))
15		rabn0 4342	. 2 ⊢ ({𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅ ↔ ∃𝑦 ∈ 𝐵 𝜑)
16		reusv2lem5 5371	. . 3 ⊢ ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶))
17		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑧 𝑥 = 𝐶
18	4	nfeq2 2941	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑧 / 𝑦⦌𝐶
19	6	eqeq2d 2773	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑧 / 𝑦⦌𝐶))
20	1, 2, 17, 18, 19	cbvrexfw 3305	. . . . 5 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)
21	9	anbi1i 636	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶))
22		anass 474	. . . . . . 7 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶)))
23	21, 22	bitri 278	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶)))
24	23	rexbii2 3107	. . . . 5 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
25	20, 24	bitr3i 280	. . . 4 ⊢ (∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
26	25	reubii 3376	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
27	1, 2, 17, 18, 19	cbvralfw 3304	. . . . 5 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)
28	9	imbi1i 352	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶))
29		impexp 456	. . . . . . 7 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶)))
30	28, 29	bitri 278	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶)))
31	30	ralbii2 3106	. . . . 5 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
32	27, 31	bitr3i 280	. . . 4 ⊢ (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
33	32	reubii 3376	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
34	16, 26, 33	3bitr3g 316	. 2 ⊢ ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
35	14, 15, 34	syl2anbr 611	1 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  ∃!wreu 3365  {crab 3414  ⦋csb 3850  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-nul 5267  ax-pow 5334

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-nul 4283

This theorem is used by:  cdleme25dN  41237