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

Theorem dfid3 5585
Description: A stronger version of df-id 5582 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 30428. 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 5582 instead to make the semantics of the constructor df-opab 5210 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 5582 . 2 I = {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧}
2 equcom 2014 . . . . . . . . . . 11 (𝑥 = 𝑧𝑧 = 𝑥)
32anbi1ci 626 . . . . . . . . . 10 ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑧 = 𝑥𝑤 = ⟨𝑥, 𝑧⟩))
43exbii 1844 . . . . . . . . 9 (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑧(𝑧 = 𝑥𝑤 = ⟨𝑥, 𝑧⟩))
5 opeq2 4878 . . . . . . . . . . 11 (𝑧 = 𝑥 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑥⟩)
65eqeq2d 2745 . . . . . . . . . 10 (𝑧 = 𝑥 → (𝑤 = ⟨𝑥, 𝑧⟩ ↔ 𝑤 = ⟨𝑥, 𝑥⟩))
76equsexvw 2001 . . . . . . . . 9 (∃𝑧(𝑧 = 𝑥𝑤 = ⟨𝑥, 𝑧⟩) ↔ 𝑤 = ⟨𝑥, 𝑥⟩)
8 equid 2008 . . . . . . . . . 10 𝑥 = 𝑥
98biantru 529 . . . . . . . . 9 (𝑤 = ⟨𝑥, 𝑥⟩ ↔ (𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
104, 7, 93bitri 297 . . . . . . . 8 (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
1110exbii 1844 . . . . . . 7 (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
12 nfe1 2147 . . . . . . . 8 𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥)
131219.9 2202 . . . . . . 7 (∃𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
1411, 13bitr4i 278 . . . . . 6 (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
15 opeq2 4878 . . . . . . . . . . 11 (𝑥 = 𝑦 → ⟨𝑥, 𝑥⟩ = ⟨𝑥, 𝑦⟩)
1615eqeq2d 2745 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑤 = ⟨𝑥, 𝑥⟩ ↔ 𝑤 = ⟨𝑥, 𝑦⟩))
17 equequ2 2022 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 = 𝑥𝑥 = 𝑦))
1816, 17anbi12d 632 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
1918sps 2182 . . . . . . . 8 (∀𝑥 𝑥 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
2019drex1 2443 . . . . . . 7 (∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
2120drex2 2444 . . . . . 6 (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
2214, 21bitrid 283 . . . . 5 (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
23 nfnae 2436 . . . . . 6 𝑥 ¬ ∀𝑥 𝑥 = 𝑦
24 nfnae 2436 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑦
25 nfcvd 2903 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑤)
26 nfcvf2 2930 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
27 nfcvd 2903 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑧)
2826, 27nfopd 4894 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥, 𝑧⟩)
2925, 28nfeqd 2913 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = ⟨𝑥, 𝑧⟩)
3026, 27nfeqd 2913 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑧)
3129, 30nfand 1894 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧))
32 opeq2 4878 . . . . . . . . . 10 (𝑧 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑦⟩)
3332eqeq2d 2745 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑤 = ⟨𝑥, 𝑧⟩ ↔ 𝑤 = ⟨𝑥, 𝑦⟩))
34 equequ2 2022 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑥 = 𝑧𝑥 = 𝑦))
3533, 34anbi12d 632 . . . . . . . 8 (𝑧 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
3635a1i 11 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦))))
3724, 31, 36cbvexd 2410 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
3823, 37exbid 2220 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
3922, 38pm2.61i 182 . . . 4 (∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦))
4039abbii 2806 . . 3 {𝑤 ∣ ∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧)} = {𝑤 ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)}
41 df-opab 5210 . . 3 {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧} = {𝑤 ∣ ∃𝑥𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧)}
42 df-opab 5210 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} = {𝑤 ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)}
4340, 41, 423eqtr4i 2772 . 2 {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧} = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
441, 43eqtri 2762 1 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wal 1534   = wceq 1536  wex 1775  {cab 2711  cop 4636  {copab 5209   I cid 5581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-13 2374  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5210  df-id 5582
This theorem is referenced by:  dfid2OLD  5586
  Copyright terms: Public domain W3C validator