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

Theorem reusv2 4795
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 3098 . . . 4 𝑦{𝑦𝐵𝜑}
2 nfcv 2750 . . . 4 𝑧{𝑦𝐵𝜑}
3 nfv 1829 . . . 4 𝑧 𝐶𝐴
4 nfcsb1v 3514 . . . . 5 𝑦𝑧 / 𝑦𝐶
54nfel1 2764 . . . 4 𝑦𝑧 / 𝑦𝐶𝐴
6 csbeq1a 3507 . . . . 5 (𝑦 = 𝑧𝐶 = 𝑧 / 𝑦𝐶)
76eleq1d 2671 . . . 4 (𝑦 = 𝑧 → (𝐶𝐴𝑧 / 𝑦𝐶𝐴))
81, 2, 3, 5, 7cbvralf 3140 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴)
9 rabid 3094 . . . . . 6 (𝑦 ∈ {𝑦𝐵𝜑} ↔ (𝑦𝐵𝜑))
109imbi1i 337 . . . . 5 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ ((𝑦𝐵𝜑) → 𝐶𝐴))
11 impexp 460 . . . . 5 (((𝑦𝐵𝜑) → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1210, 11bitri 262 . . . 4 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝐶𝐴) ↔ (𝑦𝐵 → (𝜑𝐶𝐴)))
1312ralbii2 2960 . . 3 (∀𝑦 ∈ {𝑦𝐵𝜑}𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
148, 13bitr3i 264 . 2 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ↔ ∀𝑦𝐵 (𝜑𝐶𝐴))
15 rabn0 3911 . 2 ({𝑦𝐵𝜑} ≠ ∅ ↔ ∃𝑦𝐵 𝜑)
16 reusv2lem5 4794 . . 3 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶))
17 nfv 1829 . . . . . 6 𝑧 𝑥 = 𝐶
184nfeq2 2765 . . . . . 6 𝑦 𝑥 = 𝑧 / 𝑦𝐶
196eqeq2d 2619 . . . . . 6 (𝑦 = 𝑧 → (𝑥 = 𝐶𝑥 = 𝑧 / 𝑦𝐶))
201, 2, 17, 18, 19cbvrexf 3141 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
219anbi1i 726 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶))
22 anass 678 . . . . . . 7 (((𝑦𝐵𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2321, 22bitri 262 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦𝐵 ∧ (𝜑𝑥 = 𝐶)))
2423rexbii2 3020 . . . . 5 (∃𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2520, 24bitr3i 264 . . . 4 (∃𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃𝑦𝐵 (𝜑𝑥 = 𝐶))
2625reubii 3104 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
271, 2, 17, 18, 19cbvralf 3140 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶)
289imbi1i 337 . . . . . . 7 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ ((𝑦𝐵𝜑) → 𝑥 = 𝐶))
29 impexp 460 . . . . . . 7 (((𝑦𝐵𝜑) → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3028, 29bitri 262 . . . . . 6 ((𝑦 ∈ {𝑦𝐵𝜑} → 𝑥 = 𝐶) ↔ (𝑦𝐵 → (𝜑𝑥 = 𝐶)))
3130ralbii2 2960 . . . . 5 (∀𝑦 ∈ {𝑦𝐵𝜑}𝑥 = 𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3227, 31bitr3i 264 . . . 4 (∀𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝐶))
3332reubii 3104 . . 3 (∃!𝑥𝐴𝑧 ∈ {𝑦𝐵𝜑}𝑥 = 𝑧 / 𝑦𝐶 ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶))
3416, 26, 333bitr3g 300 . 2 ((∀𝑧 ∈ {𝑦𝐵𝜑}𝑧 / 𝑦𝐶𝐴 ∧ {𝑦𝐵𝜑} ≠ ∅) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
3514, 15, 34syl2anbr 495 1 ((∀𝑦𝐵 (𝜑𝐶𝐴) ∧ ∃𝑦𝐵 𝜑) → (∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶) ↔ ∃!𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  ∃!wreu 2897  {crab 2899  csb 3498  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-nul 4712  ax-pow 4764
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-nul 3874
This theorem is referenced by:  cdleme25dN  34458
  Copyright terms: Public domain W3C validator