MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reusv2 Structured version   Visualization version   GIF version

Theorem reusv2 5363
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.
StepHypRef Expression
1 nfrab1 3429 . . . 4 𝑦{𝑦𝐵𝜑}
2 nfcv 2908 . . . 4 𝑧{𝑦𝐵𝜑}
3 nfv 1918 . . . 4 𝑧 𝐶𝐴
4 nfcsb1v 3885 . . . . 5 𝑦𝑧 / 𝑦𝐶
54nfel1 2924 . . . 4 𝑦𝑧 / 𝑦𝐶𝐴
6 csbeq1a 3874 . . . . 5 (𝑦 = 𝑧𝐶 = 𝑧 / 𝑦𝐶)
76eleq1d 2823 . . . 4 (𝑦 = 𝑧 → (𝐶𝐴𝑧 / 𝑦𝐶𝐴))
81, 2, 3, 5, 7cbvralfw 3290 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴)
9 rabid 3430 . . . . . 6 (𝑦 ∈ {𝑦𝐵𝜑} ↔ (𝑦𝐵𝜑))
109imbi1i 350 . . . . 5 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ ((𝑦𝐵𝜑) → 𝐶𝐴))
11 impexp 452 . . . . 5 (((𝑦𝐵𝜑) → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1210, 11bitri 275 . . . 4 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1312ralbii2 3093 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
148, 13bitr3i 277 . 2 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
15 rabn0 4350 . 2 ({𝑦𝐵𝜑} ≠ ∅ ↔ ∃𝑦𝐵 𝜑)
16 reusv2lem5 5362 . . 3 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶))
17 nfv 1918 . . . . . 6 𝑧 𝑥 = 𝐶
184nfeq2 2925 . . . . . 6 𝑦 𝑥 = 𝑧 / 𝑦𝐶
196eqeq2d 2748 . . . . . 6 (𝑦 = 𝑧 → (𝑥 = 𝐶𝑥 = 𝑧 / 𝑦𝐶))
201, 2, 17, 18, 19cbvrexfw 3291 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
219anbi1i 625 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶))
22 anass 470 . . . . . . 7 (((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2321, 22bitri 275 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2423rexbii2 3094 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2520, 24bitr3i 277 . . . 4 (∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2625reubii 3365 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
271, 2, 17, 18, 19cbvralfw 3290 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
289imbi1i 350 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) → 𝑥 = 𝐶))
29 impexp 452 . . . . . . 7 (((𝑦𝐵𝜑) → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3028, 29bitri 275 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3130ralbii2 3093 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3227, 31bitr3i 277 . . . 4 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3332reubii 3365 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
3416, 26, 333bitr3g 313 . 2 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
3514, 15, 34syl2anbr 600 1 ((∀𝑦𝐵 (𝜑𝐶𝐴) ∧ ∃𝑦𝐵 𝜑) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wne 2944  wral 3065  wrex 3074  ∃!wreu 3354  {crab 3410  csb 3860  c0 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-nul 5268  ax-pow 5325
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-nul 4288
This theorem is referenced by:  cdleme25dN  38848
  Copyright terms: Public domain W3C validator