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

Theorem reusv2 5409
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 3454 . . . 4 𝑦{𝑦𝐵𝜑}
2 nfcv 2903 . . . 4 𝑧{𝑦𝐵𝜑}
3 nfv 1912 . . . 4 𝑧 𝐶𝐴
4 nfcsb1v 3933 . . . . 5 𝑦𝑧 / 𝑦𝐶
54nfel1 2920 . . . 4 𝑦𝑧 / 𝑦𝐶𝐴
6 csbeq1a 3922 . . . . 5 (𝑦 = 𝑧𝐶 = 𝑧 / 𝑦𝐶)
76eleq1d 2824 . . . 4 (𝑦 = 𝑧 → (𝐶𝐴𝑧 / 𝑦𝐶𝐴))
81, 2, 3, 5, 7cbvralfw 3302 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴)
9 rabid 3455 . . . . . 6 (𝑦 ∈ {𝑦𝐵𝜑} ↔ (𝑦𝐵𝜑))
109imbi1i 349 . . . . 5 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ ((𝑦𝐵𝜑) → 𝐶𝐴))
11 impexp 450 . . . . 5 (((𝑦𝐵𝜑) → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1210, 11bitri 275 . . . 4 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1312ralbii2 3087 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
148, 13bitr3i 277 . 2 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
15 rabn0 4395 . 2 ({𝑦𝐵𝜑} ≠ ∅ ↔ ∃𝑦𝐵 𝜑)
16 reusv2lem5 5408 . . 3 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶))
17 nfv 1912 . . . . . 6 𝑧 𝑥 = 𝐶
184nfeq2 2921 . . . . . 6 𝑦 𝑥 = 𝑧 / 𝑦𝐶
196eqeq2d 2746 . . . . . 6 (𝑦 = 𝑧 → (𝑥 = 𝐶𝑥 = 𝑧 / 𝑦𝐶))
201, 2, 17, 18, 19cbvrexfw 3303 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
219anbi1i 624 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶))
22 anass 468 . . . . . . 7 (((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2321, 22bitri 275 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2423rexbii2 3088 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2520, 24bitr3i 277 . . . 4 (∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2625reubii 3387 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
271, 2, 17, 18, 19cbvralfw 3302 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
289imbi1i 349 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) → 𝑥 = 𝐶))
29 impexp 450 . . . . . . 7 (((𝑦𝐵𝜑) → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3028, 29bitri 275 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3130ralbii2 3087 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3227, 31bitr3i 277 . . . 4 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3332reubii 3387 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
3416, 26, 333bitr3g 313 . 2 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
3514, 15, 34syl2anbr 599 1 ((∀𝑦𝐵 (𝜑𝐶𝐴) ∧ ∃𝑦𝐵 𝜑) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wne 2938  wral 3059  wrex 3068  ∃!wreu 3376  {crab 3433  csb 3908  c0 4339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-nul 5312  ax-pow 5371
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-nul 4340
This theorem is referenced by:  cdleme25dN  40339
  Copyright terms: Public domain W3C validator