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

Theorem reusv2 5326
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 3317 . . . 4 𝑦{𝑦𝐵𝜑}
2 nfcv 2907 . . . 4 𝑧{𝑦𝐵𝜑}
3 nfv 1917 . . . 4 𝑧 𝐶𝐴
4 nfcsb1v 3857 . . . . 5 𝑦𝑧 / 𝑦𝐶
54nfel1 2923 . . . 4 𝑦𝑧 / 𝑦𝐶𝐴
6 csbeq1a 3846 . . . . 5 (𝑦 = 𝑧𝐶 = 𝑧 / 𝑦𝐶)
76eleq1d 2823 . . . 4 (𝑦 = 𝑧 → (𝐶𝐴𝑧 / 𝑦𝐶𝐴))
81, 2, 3, 5, 7cbvralfw 3368 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴)
9 rabid 3310 . . . . . 6 (𝑦 ∈ {𝑦𝐵𝜑} ↔ (𝑦𝐵𝜑))
109imbi1i 350 . . . . 5 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ ((𝑦𝐵𝜑) → 𝐶𝐴))
11 impexp 451 . . . . 5 (((𝑦𝐵𝜑) → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1210, 11bitri 274 . . . 4 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1312ralbii2 3090 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
148, 13bitr3i 276 . 2 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
15 rabn0 4319 . 2 ({𝑦𝐵𝜑} ≠ ∅ ↔ ∃𝑦𝐵 𝜑)
16 reusv2lem5 5325 . . 3 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶))
17 nfv 1917 . . . . . 6 𝑧 𝑥 = 𝐶
184nfeq2 2924 . . . . . 6 𝑦 𝑥 = 𝑧 / 𝑦𝐶
196eqeq2d 2749 . . . . . 6 (𝑦 = 𝑧 → (𝑥 = 𝐶𝑥 = 𝑧 / 𝑦𝐶))
201, 2, 17, 18, 19cbvrexfw 3370 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
219anbi1i 624 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶))
22 anass 469 . . . . . . 7 (((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2321, 22bitri 274 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2423rexbii2 3179 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2520, 24bitr3i 276 . . . 4 (∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2625reubii 3325 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
271, 2, 17, 18, 19cbvralfw 3368 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
289imbi1i 350 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) → 𝑥 = 𝐶))
29 impexp 451 . . . . . . 7 (((𝑦𝐵𝜑) → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3028, 29bitri 274 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3130ralbii2 3090 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3227, 31bitr3i 276 . . . 4 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3332reubii 3325 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
3416, 26, 333bitr3g 313 . 2 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
3514, 15, 34syl2anbr 599 1 ((∀𝑦𝐵 (𝜑𝐶𝐴) ∧ ∃𝑦𝐵 𝜑) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  ∃!wreu 3066  {crab 3068  csb 3832  c0 4256
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230  ax-pow 5288
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-nul 4257
This theorem is referenced by:  cdleme25dN  38370
  Copyright terms: Public domain W3C validator