Description: Alternate definition of the identity relation. Instance of dfid3 not requiring auxiliary axioms. (Contributed by NM, 15-Mar-2007) Reduce axiom usage. (Revised by GG, 4-Nov-2024) (Proof shortened by BJ, 5-Nov-2024)
Use df-id instead to make the semantics of the constructor df-opab clearer. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfid2 | ⊢ I = { ⟨ 𝑥 , 𝑥 ⟩ ∣ 𝑥 = 𝑥 } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-id | ⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } | |
| 2 | equcomi | ⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 ) | |
| 3 | 2 | opeq2d | ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ ) |
| 4 | 3 | eqeq2d | ⊢ ( 𝑥 = 𝑦 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ) ) |
| 5 | 4 | pm5.32ri | ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) ) |
| 6 | 5 | exbii | ⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) ) |
| 7 | ax6evr | ⊢ ∃ 𝑦 𝑥 = 𝑦 | |
| 8 | 19.42v | ⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ∃ 𝑦 𝑥 = 𝑦 ) ) | |
| 9 | 7 8 | mpbiran2 | ⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) ↔ 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ) |
| 10 | 6 9 | bitri | ⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ) |
| 11 | eqidd | ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ → 𝑥 = 𝑥 ) | |
| 12 | 11 | pm4.71i | ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 13 | 10 12 | bitri | ⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 14 | 13 | exbii | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 15 | id | ⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 ) | |
| 16 | 15 15 | opeq12d | ⊢ ( 𝑥 = 𝑢 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑢 , 𝑢 ⟩ ) |
| 17 | 16 | eqeq2d | ⊢ ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ↔ 𝑧 = ⟨ 𝑢 , 𝑢 ⟩ ) ) |
| 18 | 15 15 | eqeq12d | ⊢ ( 𝑥 = 𝑢 → ( 𝑥 = 𝑥 ↔ 𝑢 = 𝑢 ) ) |
| 19 | 17 18 | anbi12d | ⊢ ( 𝑥 = 𝑢 → ( ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ( 𝑧 = ⟨ 𝑢 , 𝑢 ⟩ ∧ 𝑢 = 𝑢 ) ) ) |
| 20 | 19 | exexw | ⊢ ( ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 21 | 14 20 | bitri | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ) |
| 22 | 21 | abbii | ⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) } |
| 23 | df-opab | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) } | |
| 24 | df-opab | ⊢ { ⟨ 𝑥 , 𝑥 ⟩ ∣ 𝑥 = 𝑥 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) } | |
| 25 | 22 23 24 | 3eqtr4i | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } = { ⟨ 𝑥 , 𝑥 ⟩ ∣ 𝑥 = 𝑥 } |
| 26 | 1 25 | eqtri | ⊢ I = { ⟨ 𝑥 , 𝑥 ⟩ ∣ 𝑥 = 𝑥 } |