| Metamath
Proof Explorer Theorem List (p. 74 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nvocnv 7301* | The converse of an involution is the function itself. (Contributed by Thierry Arnoux, 7-May-2019.) |
| ⊢ ((𝐹:𝐴⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥) → ◡𝐹 = 𝐹) | ||
| Theorem | f1cdmsn 7302* | If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024.) |
| ⊢ ((𝐹:𝐴–1-1→{𝐵} ∧ 𝐴 ≠ ∅) → ∃𝑥 𝐴 = {𝑥}) | ||
| Theorem | fsnex 7303* | Relate a function with a singleton as domain and one variable. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
| ⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜑)) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∃𝑓(𝑓:{𝐴}⟶𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 𝜓)) | ||
| Theorem | f1prex 7304* | Relate a one-to-one function with a pair as domain and two different variables. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
| ⊢ (𝑥 = (𝑓‘𝐴) → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = (𝑓‘𝐵) → (𝜒 ↔ 𝜑)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (∃𝑓(𝑓:{𝐴, 𝐵}–1-1→𝐷 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝜓))) | ||
| Theorem | f1ocnvdm 7305 | The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.) |
| ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴) | ||
| Theorem | f1ocnvfvrneq 7306 | If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
| ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ ran 𝐹 ∧ 𝐷 ∈ ran 𝐹)) → ((◡𝐹‘𝐶) = (◡𝐹‘𝐷) → 𝐶 = 𝐷)) | ||
| Theorem | fcof1 7307 | An application is injective if a retraction exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 11-Nov-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑅 ∘ 𝐹) = ( I ↾ 𝐴)) → 𝐹:𝐴–1-1→𝐵) | ||
| Theorem | fcofo 7308 | An application is surjective if a section exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 17-Nov-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
| ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑆:𝐵⟶𝐴 ∧ (𝐹 ∘ 𝑆) = ( I ↾ 𝐵)) → 𝐹:𝐴–onto→𝐵) | ||
| Theorem | cbvfo 7309* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
| Theorem | cbvexfo 7310* | Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) |
| ⊢ ((𝐹‘𝑥) = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐹:𝐴–onto→𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
| Theorem | cocan1 7311 | An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐹:𝐵–1-1→𝐶 ∧ 𝐻:𝐴⟶𝐵 ∧ 𝐾:𝐴⟶𝐵) → ((𝐹 ∘ 𝐻) = (𝐹 ∘ 𝐾) ↔ 𝐻 = 𝐾)) | ||
| Theorem | cocan2 7312 | A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐻 Fn 𝐵 ∧ 𝐾 Fn 𝐵) → ((𝐻 ∘ 𝐹) = (𝐾 ∘ 𝐹) ↔ 𝐻 = 𝐾)) | ||
| Theorem | fcof1oinvd 7313 | Show that a function is the inverse of a bijective function if their composition is the identity function. Formerly part of proof of fcof1o 7316. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
| Theorem | fcof1od 7314 | A function is bijective if a "retraction" and a "section" exist, see comments for fcof1 7307 and fcofo 7308. Formerly part of proof of fcof1o 7316. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
| Theorem | 2fcoidinvd 7315 | Show that a function is the inverse of a function if their compositions are the identity functions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by AV, 15-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) & ⊢ (𝜑 → (𝐹 ∘ 𝐺) = ( I ↾ 𝐵)) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
| Theorem | fcof1o 7316 | Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by AV, 15-Dec-2019.) |
| ⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐵⟶𝐴) ∧ ((𝐹 ∘ 𝐺) = ( I ↾ 𝐵) ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) → (𝐹:𝐴–1-1-onto→𝐵 ∧ ◡𝐹 = 𝐺)) | ||
| Theorem | 2fvcoidd 7317* | Show that the composition of two functions is the identity function by applying both functions to each value of the domain of the first function. (Contributed by AV, 15-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) = ( I ↾ 𝐴)) | ||
| Theorem | 2fvidf1od 7318* | A function is bijective if it has an inverse function. (Contributed by AV, 15-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) | ||
| Theorem | 2fvidinvd 7319* | Show that two functions are inverse to each other by applying them twice to each value of their domains. (Contributed by AV, 13-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 (𝐺‘(𝐹‘𝑎)) = 𝑎) & ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 (𝐹‘(𝐺‘𝑏)) = 𝑏) ⇒ ⊢ (𝜑 → ◡𝐹 = 𝐺) | ||
| Theorem | foeqcnvco 7320 | Condition for function equality in terms of vanishing of the composition with the converse. EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015.) |
| ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐺:𝐴–onto→𝐵) → (𝐹 = 𝐺 ↔ (𝐹 ∘ ◡𝐺) = ( I ↾ 𝐵))) | ||
| Theorem | f1eqcocnv 7321 | Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Proof shortened by Wolf Lammen, 29-May-2024.) |
| ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐺:𝐴–1-1→𝐵) → (𝐹 = 𝐺 ↔ (◡𝐹 ∘ 𝐺) = ( I ↾ 𝐴))) | ||
| Theorem | fveqf1o 7322 | Given a bijection 𝐹, produce another bijection 𝐺 which additionally maps two specified points. (Contributed by Mario Carneiro, 30-May-2015.) |
| ⊢ 𝐺 = (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝐶, (◡𝐹‘𝐷)})) ∪ {〈𝐶, (◡𝐹‘𝐷)〉, 〈(◡𝐹‘𝐷), 𝐶〉})) ⇒ ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐺:𝐴–1-1-onto→𝐵 ∧ (𝐺‘𝐶) = 𝐷)) | ||
| Theorem | f1ocoima 7323 | The composition of two bijections as bijection onto the image of the range of the first bijection. (Contributed by AV, 15-Aug-2025.) |
| ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐺:𝐶–1-1-onto→𝐷 ∧ 𝐵 ⊆ 𝐶) → (𝐺 ∘ 𝐹):𝐴–1-1-onto→(𝐺 “ 𝐵)) | ||
| Theorem | nf1const 7324 | A constant function from at least two elements is not one-to-one. (Contributed by AV, 30-Mar-2024.) |
| ⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1→𝐶) | ||
| Theorem | nf1oconst 7325 | A constant function from at least two elements is not bijective. (Contributed by AV, 30-Mar-2024.) |
| ⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1-onto→𝐶) | ||
| Theorem | f1ofvswap 7326 | Swapping two values in a bijection between two classes yields another bijection between those classes. (Contributed by BTernaryTau, 31-Aug-2024.) |
| ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}):𝐴–1-1-onto→𝐵) | ||
| Theorem | fvf1pr 7327 | Values of a one-to-one function between two sets with two elements. Actually, such a function is a bijection. (Contributed by AV, 22-Jul-2025.) |
| ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐹:{𝐴, 𝐵}–1-1→{𝑋, 𝑌}) → (((𝐹‘𝐴) = 𝑋 ∧ (𝐹‘𝐵) = 𝑌) ∨ ((𝐹‘𝐴) = 𝑌 ∧ (𝐹‘𝐵) = 𝑋))) | ||
| Theorem | fliftrel 7328* | 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐹 ⊆ (𝑅 × 𝑆)) | ||
| Theorem | fliftel 7329* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵))) | ||
| Theorem | fliftel1 7330* | Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴𝐹𝐵) | ||
| Theorem | fliftcnv 7331* | Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → ◡𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐵, 𝐴〉)) | ||
| Theorem | fliftfun 7332* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷))) | ||
| Theorem | fliftfund 7333* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 = 𝐶)) → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
| Theorem | fliftfuns 7334* | The function 𝐹 is the unique function defined by 𝐹‘𝐴 = 𝐵, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑧 / 𝑥⦌𝐵))) | ||
| Theorem | fliftf 7335* | The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) ⇒ ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:ran (𝑥 ∈ 𝑋 ↦ 𝐴)⟶𝑆)) | ||
| Theorem | fliftval 7336* | The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) & ⊢ (𝑥 = 𝑌 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) & ⊢ (𝜑 → Fun 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ 𝑋) → (𝐹‘𝐶) = 𝐷) | ||
| Theorem | isoeq1 7337 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
| ⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) | ||
| Theorem | isoeq2 7338 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
| ⊢ (𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑇, 𝑆 (𝐴, 𝐵))) | ||
| Theorem | isoeq3 7339 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
| ⊢ (𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑇 (𝐴, 𝐵))) | ||
| Theorem | isoeq4 7340 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
| ⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵))) | ||
| Theorem | isoeq5 7341 | Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
| ⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶))) | ||
| Theorem | nfiso 7342 | Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
| ⊢ Ⅎ𝑥𝐻 & ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝑆 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) | ||
| Theorem | isof1o 7343 | An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) | ||
| Theorem | isof1oidb 7344 | A function is a bijection iff it is an isomorphism regarding the identity relation. (Contributed by AV, 9-May-2021.) |
| ⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom I , I (𝐴, 𝐵)) | ||
| Theorem | isof1oopb 7345 | A function is a bijection iff it is an isomorphism regarding the universal class of ordered pairs as relations. (Contributed by AV, 9-May-2021.) |
| ⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻 Isom (V × V), (V × V)(𝐴, 𝐵)) | ||
| Theorem | isorel 7346 | An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.) |
| ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) | ||
| Theorem | soisores 7347* | Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015.) |
| ⊢ (((𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶) ∧ (𝐹:𝐵⟶𝐶 ∧ 𝐴 ⊆ 𝐵)) → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, (𝐹 “ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐹‘𝑥)𝑆(𝐹‘𝑦)))) | ||
| Theorem | soisoi 7348* | Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
| ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
| Theorem | isoid 7349 | Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
| ⊢ ( I ↾ 𝐴) Isom 𝑅, 𝑅 (𝐴, 𝐴) | ||
| Theorem | isocnv 7350 | Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴)) | ||
| Theorem | isocnv2 7351 | Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom ◡𝑅, ◡𝑆(𝐴, 𝐵)) | ||
| Theorem | isocnv3 7352 | Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ 𝐶 = ((𝐴 × 𝐴) ∖ 𝑅) & ⊢ 𝐷 = ((𝐵 × 𝐵) ∖ 𝑆) ⇒ ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝐶, 𝐷 (𝐴, 𝐵)) | ||
| Theorem | isores2 7353 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, (𝑆 ∩ (𝐵 × 𝐵))(𝐴, 𝐵)) | ||
| Theorem | isores1 7354 | An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom (𝑅 ∩ (𝐴 × 𝐴)), 𝑆(𝐴, 𝐵)) | ||
| Theorem | isores3 7355 | Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.) |
| ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐾 ⊆ 𝐴 ∧ 𝑋 = (𝐻 “ 𝐾)) → (𝐻 ↾ 𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋)) | ||
| Theorem | isotr 7356 | Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
| ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑆, 𝑇 (𝐵, 𝐶)) → (𝐺 ∘ 𝐻) Isom 𝑅, 𝑇 (𝐴, 𝐶)) | ||
| Theorem | isomin 7357 | Isomorphisms preserve minimal elements. Note that (◡𝑅 “ {𝐷}) is Takeuti and Zaring's idiom for the initial segment {𝑥 ∣ 𝑥𝑅𝐷}. Proposition 6.31(1) of [TakeutiZaring] p. 33. (Contributed by NM, 19-Apr-2004.) |
| ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐶 ∩ (◡𝑅 “ {𝐷})) = ∅ ↔ ((𝐻 “ 𝐶) ∩ (◡𝑆 “ {(𝐻‘𝐷)})) = ∅)) | ||
| Theorem | isoini 7358 | Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.) |
| ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐷 ∈ 𝐴) → (𝐻 “ (𝐴 ∩ (◡𝑅 “ {𝐷}))) = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝐷)}))) | ||
| Theorem | isoini2 7359 | Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.) |
| ⊢ 𝐶 = (𝐴 ∩ (◡𝑅 “ {𝑋})) & ⊢ 𝐷 = (𝐵 ∩ (◡𝑆 “ {(𝐻‘𝑋)})) ⇒ ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝑋 ∈ 𝐴) → (𝐻 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷)) | ||
| Theorem | isofrlem 7360* | Lemma for isofr 7362. (Contributed by NM, 29-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.) |
| ⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V) ⇒ ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴)) | ||
| Theorem | isoselem 7361* | Lemma for isose 7363. (Contributed by Mario Carneiro, 23-Jun-2015.) |
| ⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V) ⇒ ⊢ (𝜑 → (𝑅 Se 𝐴 → 𝑆 Se 𝐵)) | ||
| Theorem | isofr 7362 | An isomorphism preserves well-foundedness. Proposition 6.32(1) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵)) | ||
| Theorem | isose 7363 | An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵)) | ||
| Theorem | isofr2 7364 | A weak form of isofr 7362 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.) |
| ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐵 ∈ 𝑉) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴)) | ||
| Theorem | isopolem 7365 | Lemma for isopo 7366. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵 → 𝑅 Po 𝐴)) | ||
| Theorem | isopo 7366 | An isomorphism preserves the property of being a partial order. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐵)) | ||
| Theorem | isosolem 7367 | Lemma for isoso 7368. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵 → 𝑅 Or 𝐴)) | ||
| Theorem | isoso 7368 | An isomorphism preserves the property of being a strict total order. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) | ||
| Theorem | isowe 7369 | An isomorphism preserves the property of being a well-ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 18-Nov-2014.) |
| ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵)) | ||
| Theorem | isowe2 7370* | A weak form of isowe 7369 that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014.) |
| ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ ∀𝑥(𝐻 “ 𝑥) ∈ V) → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
| Theorem | f1oiso 7371* | Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.) |
| ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑆 = {〈𝑧, 𝑤〉 ∣ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑧 = (𝐻‘𝑥) ∧ 𝑤 = (𝐻‘𝑦)) ∧ 𝑥𝑅𝑦)}) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
| Theorem | f1oiso2 7372* | Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. (Contributed by Mario Carneiro, 9-Mar-2013.) |
| ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (◡𝐻‘𝑥)𝑅(◡𝐻‘𝑦))} ⇒ ⊢ (𝐻:𝐴–1-1-onto→𝐵 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) | ||
| Theorem | f1owe 7373* | Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997.) |
| ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝐹‘𝑥)𝑆(𝐹‘𝑦)} ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑆 We 𝐵 → 𝑅 We 𝐴)) | ||
| Theorem | weniso 7374 | A set-like well-ordering has no nontrivial automorphisms. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.) |
| ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴)) | ||
| Theorem | weisoeq 7375 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso 7998. (Contributed by Mario Carneiro, 25-Jun-2015.) |
| ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺) | ||
| Theorem | weisoeq2 7376 | Thus, there is at most one isomorphism between any two set-like well-ordered classes. Class version of wemoiso2 7999. (Contributed by Mario Carneiro, 25-Jun-2015.) |
| ⊢ (((𝑆 We 𝐵 ∧ 𝑆 Se 𝐵) ∧ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) → 𝐹 = 𝐺) | ||
| Theorem | knatar 7377* | The Knaster-Tarski theorem says that every monotone function over a complete lattice has a (least) fixpoint. Here we specialize this theorem to the case when the lattice is the powerset lattice 𝒫 𝐴. (Contributed by Mario Carneiro, 11-Jun-2015.) |
| ⊢ 𝑋 = ∩ {𝑧 ∈ 𝒫 𝐴 ∣ (𝐹‘𝑧) ⊆ 𝑧} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹‘𝐴) ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝑥(𝐹‘𝑦) ⊆ (𝐹‘𝑥)) → (𝑋 ⊆ 𝐴 ∧ (𝐹‘𝑋) = 𝑋)) | ||
| Theorem | fvresval 7378 | The value of a restricted function at a class is either the empty set or the value of the unrestricted function at that class. (Contributed by Scott Fenton, 4-Sep-2011.) |
| ⊢ (((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴) ∨ ((𝐹 ↾ 𝐵)‘𝐴) = ∅) | ||
| Theorem | funeldmb 7379 | If ∅ is not part of the range of a function 𝐹, then 𝐴 is in the domain of 𝐹 iff (𝐹‘𝐴) ≠ ∅. (Contributed by Scott Fenton, 7-Dec-2021.) |
| ⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹) → (𝐴 ∈ dom 𝐹 ↔ (𝐹‘𝐴) ≠ ∅)) | ||
| Theorem | eqfunresadj 7380 | Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌}))) | ||
| Theorem | eqfunressuc 7381 | Law for equality of restriction to successors. This is primarily useful when 𝑋 is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.) |
| ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑋 ∈ dom 𝐹 ∧ 𝑋 ∈ dom 𝐺 ∧ (𝐹‘𝑋) = (𝐺‘𝑋))) → (𝐹 ↾ suc 𝑋) = (𝐺 ↾ suc 𝑋)) | ||
| Theorem | fnssintima 7382* | Condition for subset of an intersection of an image. (Contributed by Scott Fenton, 16-Aug-2024.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ ∩ (𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥))) | ||
| Theorem | imaeqsexvOLD 7383* | Obsolete version of rexima 7258 as of 14-Aug-2025. Duplicate version of rexima 7258. (Contributed by Scott Fenton, 27-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)) | ||
| Theorem | imaeqsalvOLD 7384* | Obsolete version of ralima 7257 as of 14-Aug-2025. Duplicate version of ralima 7257. (Contributed by Scott Fenton, 27-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ (𝐹 “ 𝐵)𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)) | ||
| Theorem | canth 7385 | No set 𝐴 is equinumerous to its power set (Cantor's theorem), i.e., no function can map 𝐴 onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. For the equinumerosity version, see canth2 9170. Note that 𝐴 must be a set: this theorem does not hold when 𝐴 is too large to be a set; see ncanth 7386 for a counterexample. (Use nex 1800 if you want the form ¬ ∃𝑓𝑓:𝐴–onto→𝒫 𝐴.) (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ¬ 𝐹:𝐴–onto→𝒫 𝐴 | ||
| Theorem | ncanth 7386 |
Cantor's theorem fails for the universal class (which is not a set but a
proper class by vprc 5315). Specifically, the identity function maps
the
universe onto its power class. Compare canth 7385 that works for sets.
This failure comes from a limitation of the collection principle (which is necessary to avoid Russell's paradox ru 3786): 𝒫 V, being a class, cannot contain proper classes, so it is no larger than V, which is why the identity function "succeeds" in being surjective onto 𝒫 V (see pwv 4904). See also the remark in ru 3786 about NF, in which Cantor's theorem fails for sets that are "too large". This theorem gives some intuition behind that failure: in NF the universal class is a set, and it equals its own power set. (Contributed by NM, 29-Jun-2004.) (Proof shortened by BJ, 29-Dec-2023.) |
| ⊢ I :V–onto→𝒫 V | ||
| Syntax | crio 7387 | Extend class notation with restricted description binder. |
| class (℩𝑥 ∈ 𝐴 𝜑) | ||
| Definition | df-riota 7388 | Define restricted description binder. In case there is no unique 𝑥 such that (𝑥 ∈ 𝐴 ∧ 𝜑) holds, it evaluates to the empty set. See also comments for df-iota 6514. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
| ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
| Theorem | riotaeqdv 7389* | Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜓)) | ||
| Theorem | riotabidv 7390* | Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) | ||
| Theorem | riotaeqbidv 7391* | Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) | ||
| Theorem | riotaex 7392 | Restricted iota is a set. (Contributed by NM, 15-Sep-2011.) |
| ⊢ (℩𝑥 ∈ 𝐴 𝜓) ∈ V | ||
| Theorem | riotav 7393 | An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.) |
| ⊢ (℩𝑥 ∈ V 𝜑) = (℩𝑥𝜑) | ||
| Theorem | riotauni 7394 | Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.) |
| ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) = ∪ {𝑥 ∈ 𝐴 ∣ 𝜑}) | ||
| Theorem | nfriota1 7395* | The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐴 𝜑) | ||
| Theorem | nfriotadw 7396* | Deduction version of nfriota 7400 with a disjoint variable condition, which contrary to nfriotad 7399 does not require ax-13 2377. (Contributed by NM, 18-Feb-2013.) Avoid ax-13 2377. (Revised by GG, 26-Jan-2024.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓)) | ||
| Theorem | cbvriotaw 7397* | Change bound variable in a restricted description binder. Version of cbvriota 7401 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 18-Mar-2013.) Avoid ax-13 2377. (Revised by GG, 26-Jan-2024.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
| Theorem | cbvriotavw 7398* | Change bound variable in a restricted description binder. Version of cbvriotav 7402 with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓) | ||
| Theorem | nfriotad 7399 | Deduction version of nfriota 7400. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker nfriotadw 7396 when possible. (Contributed by NM, 18-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓)) | ||
| Theorem | nfriota 7400* | A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜑) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |