ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  reu8 GIF version

Theorem reu8 2880
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 2656 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑦𝐴 𝜓)
3 reu6 2873 . 2 (∃!𝑦𝐴 𝜓 ↔ ∃𝑥𝐴𝑦𝐴 (𝜓𝑦 = 𝑥))
4 dfbi2 385 . . . . 5 ((𝜓𝑦 = 𝑥) ↔ ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)))
54ralbii 2441 . . . 4 (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ ∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)))
6 ancom 264 . . . . . 6 ((𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)) ↔ (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ∧ 𝜑))
7 equcom 1682 . . . . . . . . . 10 (𝑥 = 𝑦𝑦 = 𝑥)
87imbi2i 225 . . . . . . . . 9 ((𝜓𝑥 = 𝑦) ↔ (𝜓𝑦 = 𝑥))
98ralbii 2441 . . . . . . . 8 (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ↔ ∀𝑦𝐴 (𝜓𝑦 = 𝑥))
109a1i 9 . . . . . . 7 (𝑥𝐴 → (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ↔ ∀𝑦𝐴 (𝜓𝑦 = 𝑥)))
11 biimt 240 . . . . . . . 8 (𝑥𝐴 → (𝜑 ↔ (𝑥𝐴𝜑)))
12 df-ral 2421 . . . . . . . . 9 (∀𝑦𝐴 (𝑦 = 𝑥𝜓) ↔ ∀𝑦(𝑦𝐴 → (𝑦 = 𝑥𝜓)))
13 bi2.04 247 . . . . . . . . . 10 ((𝑦𝐴 → (𝑦 = 𝑥𝜓)) ↔ (𝑦 = 𝑥 → (𝑦𝐴𝜓)))
1413albii 1446 . . . . . . . . 9 (∀𝑦(𝑦𝐴 → (𝑦 = 𝑥𝜓)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦𝐴𝜓)))
15 vex 2689 . . . . . . . . . 10 𝑥 ∈ V
16 eleq1 2202 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1716, 1imbi12d 233 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
1817bicomd 140 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑦𝐴𝜓) ↔ (𝑥𝐴𝜑)))
1918equcoms 1684 . . . . . . . . . 10 (𝑦 = 𝑥 → ((𝑦𝐴𝜓) ↔ (𝑥𝐴𝜑)))
2015, 19ceqsalv 2716 . . . . . . . . 9 (∀𝑦(𝑦 = 𝑥 → (𝑦𝐴𝜓)) ↔ (𝑥𝐴𝜑))
2112, 14, 203bitrri 206 . . . . . . . 8 ((𝑥𝐴𝜑) ↔ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))
2211, 21syl6bb 195 . . . . . . 7 (𝑥𝐴 → (𝜑 ↔ ∀𝑦𝐴 (𝑦 = 𝑥𝜓)))
2310, 22anbi12d 464 . . . . . 6 (𝑥𝐴 → ((∀𝑦𝐴 (𝜓𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))))
246, 23syl5bb 191 . . . . 5 (𝑥𝐴 → ((𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))))
25 r19.26 2558 . . . . 5 (∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓)))
2624, 25syl6rbbr 198 . . . 4 (𝑥𝐴 → (∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)) ↔ (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦))))
275, 26syl5bb 191 . . 3 (𝑥𝐴 → (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦))))
2827rexbiia 2450 . 2 (∃𝑥𝐴𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))
292, 3, 283bitri 205 1 (∃!𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1329  wcel 1480  wral 2416  wrex 2417  ∃!wreu 2418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-clab 2126  df-cleq 2132  df-clel 2135  df-ral 2421  df-rex 2422  df-reu 2423  df-v 2688
This theorem is referenced by:  updjud  6970
  Copyright terms: Public domain W3C validator