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

Theorem dfid3 5583
Description: A stronger version of df-id 5580 that does not require 𝑥 and 𝑦 to be disjoint. This is not the definition since, in order to pass our definition soundness test, a definition has to have disjoint dummy variables, see conventions 30333. The proof can be instructive in showing how disjoint variable conditions may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.)

Use df-id 5580 instead to make the semantics of the constructor df-opab 5216 clearer (in usages, 𝑥, 𝑦 will typically be dummy variables, so can be assumed disjoint). (New usage is discouraged.)

Assertion
Ref Expression
dfid3 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}

Proof of Theorem dfid3
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-id 5580 . 2 I = {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧}
2 equcom 2014 . . . . . . . . . . 11 (𝑥 = 𝑧𝑧 = 𝑥)
32anbi1ci 624 . . . . . . . . . 10 ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑧 = 𝑥𝑤 = ⟨𝑥, 𝑧⟩))
43exbii 1843 . . . . . . . . 9 (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑧(𝑧 = 𝑥𝑤 = ⟨𝑥, 𝑧⟩))
5 opeq2 4880 . . . . . . . . . . 11 (𝑧 = 𝑥 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑥⟩)
65eqeq2d 2737 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑤 = ⟨𝑥, 𝑧⟩ ↔ 𝑤 = ⟨𝑥, 𝑥⟩))
76equsexvw 2001 . . . . . . . . 9 (∃𝑧(𝑧 = 𝑥𝑤 = ⟨𝑥, 𝑧⟩) ↔ 𝑤 = ⟨𝑥, 𝑥⟩)
8 equid 2008 . . . . . . . . . 10 𝑥 = 𝑥
98biantru 528 . . . . . . . . 9 (𝑤 = ⟨𝑥, 𝑥⟩ ↔ (𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
104, 7, 93bitri 296 . . . . . . . 8 (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
1110exbii 1843 . . . . . . 7 (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
12 nfe1 2140 . . . . . . . 8 𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥)
131219.9 2194 . . . . . . 7 (∃𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
1411, 13bitr4i 277 . . . . . 6 (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
15 opeq2 4880 . . . . . . . . . . 11 (𝑥 = 𝑦 → ⟨𝑥, 𝑥⟩ = ⟨𝑥, 𝑦⟩)
1615eqeq2d 2737 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑤 = ⟨𝑥, 𝑥⟩ ↔ 𝑤 = ⟨𝑥, 𝑦⟩))
17 equequ2 2022 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 = 𝑥𝑥 = 𝑦))
1816, 17anbi12d 630 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
1918sps 2174 . . . . . . . 8 (∀𝑥 𝑥 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
2019drex1 2435 . . . . . . 7 (∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
2120drex2 2436 . . . . . 6 (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
2214, 21bitrid 282 . . . . 5 (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
23 nfnae 2428 . . . . . 6 𝑥 ¬ ∀𝑥 𝑥 = 𝑦
24 nfnae 2428 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑦
25 nfcvd 2893 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑤)
26 nfcvf2 2923 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
27 nfcvd 2893 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑧)
2826, 27nfopd 4896 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥, 𝑧⟩)
2925, 28nfeqd 2903 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = ⟨𝑥, 𝑧⟩)
3026, 27nfeqd 2903 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑧)
3129, 30nfand 1893 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧))
32 opeq2 4880 . . . . . . . . . 10 (𝑧 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑦⟩)
3332eqeq2d 2737 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑤 = ⟨𝑥, 𝑧⟩ ↔ 𝑤 = ⟨𝑥, 𝑦⟩))
34 equequ2 2022 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑥 = 𝑧𝑥 = 𝑦))
3533, 34anbi12d 630 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
3635a1i 11 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦))))
3724, 31, 36cbvexd 2402 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
3823, 37exbid 2212 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
3922, 38pm2.61i 182 . . . 4 (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦))
4039abbii 2796 . . 3 {𝑤 ∣ ∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧)} = {𝑤 ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)}
41 df-opab 5216 . . 3 {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧} = {𝑤 ∣ ∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧)}
42 df-opab 5216 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} = {𝑤 ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)}
4340, 41, 423eqtr4i 2764 . 2 {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧} = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
441, 43eqtri 2754 1 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wal 1532   = wceq 1534  wex 1774  {cab 2703  cop 4639  {copab 5215   I cid 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-13 2366  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-opab 5216  df-id 5580
This theorem is referenced by:  dfid2OLD  5584
  Copyright terms: Public domain W3C validator