Description: A stronger version of df-id that does not require x and y 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 . 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 instead to make the semantics of the constructor df-opab clearer (in usages, x , y will typically be dummy variables, so can be assumed disjoint). (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfid3 | ⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-id | ⊢ I = { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝑥 = 𝑧 } | |
| 2 | equcom | ⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 ) | |
| 3 | 2 | anbi1ci | ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ) ) |
| 4 | 3 | exbii | ⊢ ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ) ) |
| 5 | opeq2 | ⊢ ( 𝑧 = 𝑥 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ ) | |
| 6 | 5 | eqeq2d | ⊢ ( 𝑧 = 𝑥 → ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ↔ 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ) ) |
| 7 | 6 | equsexvw | ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ) ↔ 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ) |
| 8 | equid | ⊢ 𝑥 = 𝑥 | |
| 9 | 8 | biantru | ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 10 | 4 7 9 | 3bitri | ⊢ ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 11 | 10 | exbii | ⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 12 | nfe1 | ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) | |
| 13 | 12 | 19.9 | ⊢ ( ∃ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 14 | 11 13 | bitr4i | ⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 15 | opeq2 | ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) | |
| 16 | 15 | eqeq2d | ⊢ ( 𝑥 = 𝑦 → ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ↔ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ) |
| 17 | equequ2 | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑥 ↔ 𝑥 = 𝑦 ) ) | |
| 18 | 16 17 | anbi12d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 19 | 18 | sps | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 20 | 19 | drex1 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 21 | 20 | drex2 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 22 | 14 21 | syl5bb | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 23 | nfnae | ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 | |
| 24 | nfnae | ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 | |
| 25 | nfcvd | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 ) | |
| 26 | nfcvf2 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ) | |
| 27 | nfcvd | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑧 ) | |
| 28 | 26 27 | nfopd | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ⟨ 𝑥 , 𝑧 ⟩ ) |
| 29 | 25 28 | nfeqd | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ) |
| 30 | 26 27 | nfeqd | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 = 𝑧 ) |
| 31 | 29 30 | nfand | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ) |
| 32 | opeq2 | ⊢ ( 𝑧 = 𝑦 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) | |
| 33 | 32 | eqeq2d | ⊢ ( 𝑧 = 𝑦 → ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ↔ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ) |
| 34 | equequ2 | ⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) ) | |
| 35 | 33 34 | anbi12d | ⊢ ( 𝑧 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 36 | 35 | a1i | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) ) |
| 37 | 24 31 36 | cbvexd | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 38 | 23 37 | exbid | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) |
| 39 | 22 38 | pm2.61i | ⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) |
| 40 | 39 | abbii | ⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) } |
| 41 | df-opab | ⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝑥 = 𝑧 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) } | |
| 42 | df-opab | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) } | |
| 43 | 40 41 42 | 3eqtr4i | ⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝑥 = 𝑧 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } |
| 44 | 1 43 | eqtri | ⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } |