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

Theorem reu8 2802
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 2588 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑦𝐴 𝜓)
3 reu6 2795 . 2 (∃!𝑦𝐴 𝜓 ↔ ∃𝑥𝐴𝑦𝐴 (𝜓𝑦 = 𝑥))
4 dfbi2 380 . . . . 5 ((𝜓𝑦 = 𝑥) ↔ ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)))
54ralbii 2380 . . . 4 (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ ∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)))
6 ancom 262 . . . . . 6 ((𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)) ↔ (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ∧ 𝜑))
7 equcom 1637 . . . . . . . . . 10 (𝑥 = 𝑦𝑦 = 𝑥)
87imbi2i 224 . . . . . . . . 9 ((𝜓𝑥 = 𝑦) ↔ (𝜓𝑦 = 𝑥))
98ralbii 2380 . . . . . . . 8 (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ↔ ∀𝑦𝐴 (𝜓𝑦 = 𝑥))
109a1i 9 . . . . . . 7 (𝑥𝐴 → (∀𝑦𝐴 (𝜓𝑥 = 𝑦) ↔ ∀𝑦𝐴 (𝜓𝑦 = 𝑥)))
11 biimt 239 . . . . . . . 8 (𝑥𝐴 → (𝜑 ↔ (𝑥𝐴𝜑)))
12 df-ral 2360 . . . . . . . . 9 (∀𝑦𝐴 (𝑦 = 𝑥𝜓) ↔ ∀𝑦(𝑦𝐴 → (𝑦 = 𝑥𝜓)))
13 bi2.04 246 . . . . . . . . . 10 ((𝑦𝐴 → (𝑦 = 𝑥𝜓)) ↔ (𝑦 = 𝑥 → (𝑦𝐴𝜓)))
1413albii 1402 . . . . . . . . 9 (∀𝑦(𝑦𝐴 → (𝑦 = 𝑥𝜓)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦𝐴𝜓)))
15 vex 2618 . . . . . . . . . 10 𝑥 ∈ V
16 eleq1 2147 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
1716, 1imbi12d 232 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
1817bicomd 139 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑦𝐴𝜓) ↔ (𝑥𝐴𝜑)))
1918equcoms 1638 . . . . . . . . . 10 (𝑦 = 𝑥 → ((𝑦𝐴𝜓) ↔ (𝑥𝐴𝜑)))
2015, 19ceqsalv 2643 . . . . . . . . 9 (∀𝑦(𝑦 = 𝑥 → (𝑦𝐴𝜓)) ↔ (𝑥𝐴𝜑))
2112, 14, 203bitrri 205 . . . . . . . 8 ((𝑥𝐴𝜑) ↔ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))
2211, 21syl6bb 194 . . . . . . 7 (𝑥𝐴 → (𝜑 ↔ ∀𝑦𝐴 (𝑦 = 𝑥𝜓)))
2310, 22anbi12d 457 . . . . . 6 (𝑥𝐴 → ((∀𝑦𝐴 (𝜓𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))))
246, 23syl5bb 190 . . . . 5 (𝑥𝐴 → ((𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓))))
25 r19.26 2493 . . . . 5 (∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)) ↔ (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ∧ ∀𝑦𝐴 (𝑦 = 𝑥𝜓)))
2624, 25syl6rbbr 197 . . . 4 (𝑥𝐴 → (∀𝑦𝐴 ((𝜓𝑦 = 𝑥) ∧ (𝑦 = 𝑥𝜓)) ↔ (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦))))
275, 26syl5bb 190 . . 3 (𝑥𝐴 → (∀𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦))))
2827rexbiia 2389 . 2 (∃𝑥𝐴𝑦𝐴 (𝜓𝑦 = 𝑥) ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))
292, 3, 283bitri 204 1 (∃!𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 (𝜑 ∧ ∀𝑦𝐴 (𝜓𝑥 = 𝑦)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wal 1285  wcel 1436  wral 2355  wrex 2356  ∃!wreu 2357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-clab 2072  df-cleq 2078  df-clel 2081  df-ral 2360  df-rex 2361  df-reu 2362  df-v 2617
This theorem is referenced by:  updjud  6720
  Copyright terms: Public domain W3C validator