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

Theorem reu8 3658
Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.)
Hypothesis
Ref Expression
rmo4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
reu8 (∃!𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem reu8
StepHypRef Expression
1 rmo4.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21cbvreuv 3405 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑦𝐴 𝜓)
3 reu6 3651 . 2 (∃!𝑦𝐴 𝜓 ↔ ∃𝑥𝐴𝑦𝐴 (𝜓𝑦 = 𝑥))
4 dfbi2 475 . . . . 5 ((𝜓𝑦 = 𝑥) ↔ ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)))
54ralbii 3132 . . . 4 (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ ∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)))
6 ancom 461 . . . . . 6 ((𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)) ↔ (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ∧ 𝜑))
7 equcom 2002 . . . . . . . . . 10 (𝑥 = 𝑦𝑦 = 𝑥)
87imbi2i 337 . . . . . . . . 9 ((𝜓𝑥 = 𝑦) ↔ (𝜓𝑦 = 𝑥))
98ralbii 3132 . . . . . . . 8 (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ↔ ∀𝑦𝐴 (𝜓𝑦 = 𝑥))
109a1i 11 . . . . . . 7 (𝑥𝐴 → (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ↔ ∀𝑦𝐴 (𝜓𝑦 = 𝑥)))
11 biimt 362 . . . . . . . 8 (𝑥𝐴 → (𝜑 ↔ (𝑥𝐴𝜑)))
12 df-ral 3110 . . . . . . . . 9 (∀𝑦𝐴 (𝑦 = 𝑥𝜓) ↔ ∀𝑦(𝑦𝐴 → (𝑦 = 𝑥𝜓)))
13 bi2.04 389 . . . . . . . . . 10 ((𝑦𝐴 → (𝑦 = 𝑥𝜓)) ↔ (𝑦 = 𝑥 → (𝑦𝐴𝜓)))
1413albii 1801 . . . . . . . . 9 (∀𝑦(𝑦𝐴 → (𝑦 = 𝑥𝜓)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦𝐴𝜓)))
15 eleq1w 2865 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1615, 1imbi12d 346 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
1716bicomd 224 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑦𝐴𝜓) ↔ (𝑥𝐴𝜑)))
1817equcoms 2004 . . . . . . . . . 10 (𝑦 = 𝑥 → ((𝑦𝐴𝜓) ↔ (𝑥𝐴𝜑)))
1918equsalvw 1987 . . . . . . . . 9 (∀𝑦(𝑦 = 𝑥 → (𝑦𝐴𝜓)) ↔ (𝑥𝐴𝜑))
2012, 14, 193bitrri 299 . . . . . . . 8 ((𝑥𝐴𝜑) ↔ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))
2111, 20syl6bb 288 . . . . . . 7 (𝑥𝐴 → (𝜑 ↔ ∀𝑦𝐴 (𝑦 = 𝑥𝜓)))
2210, 21anbi12d 630 . . . . . 6 (𝑥𝐴 → ((∀𝑦𝐴 (𝜓𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))))
236, 22syl5bb 284 . . . . 5 (𝑥𝐴 → ((𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))))
24 r19.26 3137 . . . . 5 (∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓)))
2523, 24syl6rbbr 291 . . . 4 (𝑥𝐴 → (∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)) ↔ (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦))))
265, 25syl5bb 284 . . 3 (𝑥𝐴 → (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦))))
2726rexbiia 3210 . 2 (∃𝑥𝐴𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))
282, 3, 273bitri 298 1 (∃!𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1520  wcel 2081  wral 3105  wrex 3106  ∃!wreu 3107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clel 2863  df-ral 3110  df-rex 3111  df-reu 3112
This theorem is referenced by:  reu8nf  3788  updjud  9209  reusq0  14656  reumodprminv  15970  grpinveu  17895  addsq2reu  25698  2sqreulem1  25704  2sqreunnlem1  25707  grpoideu  27977  grpoinveu  27987  cvmlift3lem2  32175  euoreqb  42824  2reu8i  42828  2reuimp0  42829  paireqne  43155  itsclquadeu  44245
  Copyright terms: Public domain W3C validator