| Metamath
Proof Explorer Theorem List (p. 363 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 | ixpeq1i 36201 | Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶 | ||
| Theorem | ixpeq12i 36202 | Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | sumeq2si 36203 | Equality inference for sum. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐵 = 𝐶 ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | sumeq12si 36204 | Equality inference for sum. General version of sumeq2si 36203. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | prodeq2si 36205 | Equality inference for product. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐵 = 𝐶 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | prodeq12si 36206 | Equality inference for product. General version of prodeq2si 36205. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | itgeq12i 36207 | Equality inference for an integral. General version of itgeq1i 36208 and itgeq2i 36209. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥 | ||
| Theorem | itgeq1i 36208 | Equality inference for an integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥 | ||
| Theorem | itgeq2i 36209 | Equality inference for an integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐵 = 𝐶 ⇒ ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥 | ||
| Theorem | ditgeq123i 36210 | Equality inference for the directed integral. General version of ditgeq12i 36211 and ditgeq3i 36212. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 & ⊢ 𝐸 = 𝐹 ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥 | ||
| Theorem | ditgeq12i 36211 | Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥 | ||
| Theorem | ditgeq3i 36212 | Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐶 = 𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥 | ||
| Theorem | rmoeqdv 36213* | Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) | ||
| Theorem | rmoeqbidv 36214* | Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3397. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)) | ||
| Theorem | sbequbidv 36215* | Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝑢 = 𝑣) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒)) | ||
| Theorem | disjeq12dv 36216* | Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)) | ||
| Theorem | ixpeq12dv 36217* | Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷) | ||
| Theorem | sumeq12sdv 36218* | Equality deduction for sum. General version of sumeq2sdv 15739. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | prodeq12sdv 36219* | Equality deduction for product. General version of prodeq2sdv 15959. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | itgeq12sdv 36220* | Equality theorem for an integral. Deduction form. General version of itgeq1d 45972 and itgeq2sdv 36221. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥) | ||
| Theorem | itgeq2sdv 36221* | Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥) | ||
| Theorem | ditgeq123dv 36222* | Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv 36224. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥) | ||
| Theorem | ditgeq12d 36223* | Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥) | ||
| Theorem | ditgeq3sdv 36224* | Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥) | ||
| Theorem | in-ax8 36225 | A proof of ax-8 2110 that does not rely on ax-8 2110. It employs df-in 3958 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2118. Since the nature of this result is unclear, usage of this theorem is discouraged, and this method should not be applied to eliminate axiom dependencies. (Contributed by GG, 1-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
| Theorem | ss-ax8 36226 | A proof of ax-8 2110 that does not rely on ax-8 2110. It employs df-ss 3968 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2118. Contrary to in-ax8 36225, this proof does not rely on df-cleq 2729, therefore using fewer axioms . This method should not be applied to eliminate axiom dependencies. (Contributed by GG, 30-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)) | ||
| Theorem | cbvralvw2 36227* | Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) | ||
| Theorem | cbvrexvw2 36228* | Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) | ||
| Theorem | cbvrmovw2 36229* | Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓) | ||
| Theorem | cbvreuvw2 36230* | Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓) | ||
| Theorem | cbvsbcvw2 36231* | Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3822. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓) | ||
| Theorem | cbvcsbvw2 36232* | Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv 3911. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷 | ||
| Theorem | cbviunvw2 36233* | Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷 | ||
| Theorem | cbviinvw2 36234* | Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷 | ||
| Theorem | cbvmptvw2 36235* | Change bound variable and domain in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷) | ||
| Theorem | cbvdisjvw2 36236* | Change bound variable and domain in a disjoint collection, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷) | ||
| Theorem | cbvriotavw2 36237* | Change bound variable and domain in a restricted description binder, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐵 𝜓) | ||
| Theorem | cbvoprab1vw 36238* | Change the first bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑤 → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑧〉 ∣ 𝜒} | ||
| Theorem | cbvoprab2vw 36239* | Change the second bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑧〉 ∣ 𝜒} | ||
| Theorem | cbvoprab123vw 36240* | Change all bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑢〉, 𝑣〉 ∣ 𝜒} | ||
| Theorem | cbvoprab23vw 36241* | Change the second and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑣〉 ∣ 𝜒} | ||
| Theorem | cbvoprab13vw 36242* | Change the first and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝑥 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑣〉 ∣ 𝜒} | ||
| Theorem | cbvmpovw2 36243* | Change bound variables and domains in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹) & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹) | ||
| Theorem | cbvmpo1vw2 36244* | Change domains and the first bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑧 → 𝐸 = 𝐹) & ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑧 → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹) | ||
| Theorem | cbvmpo2vw2 36245* | Change domains and the second bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑦 = 𝑧 → 𝐸 = 𝐹) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) & ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹) | ||
| Theorem | cbvixpvw2 36246* | Change bound variable and domain in an indexed Cartesian product, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷 | ||
| Theorem | cbvsumvw2 36247* | Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷) ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷 | ||
| Theorem | cbvprodvw2 36248* | Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷 | ||
| Theorem | cbvitgvw2 36249* | Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦 | ||
| Theorem | cbvditgvw2 36250* | Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 & ⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹) ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦 | ||
| Theorem | cbvmodavw 36251* | Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑦𝜒)) | ||
| Theorem | cbveudavw 36252* | Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒)) | ||
| Theorem | cbvrmodavw 36253* | Change bound variable in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐴 𝜒)) | ||
| Theorem | cbvreudavw 36254* | Change bound variable in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒)) | ||
| Theorem | cbvsbdavw 36255* | Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑦]𝜒)) | ||
| Theorem | cbvsbdavw2 36256* | Change bound variable in proper substitution. General version of cbvsbdavw 36255. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝜑 → 𝑧 = 𝑤) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑤 / 𝑦]𝜒)) | ||
| Theorem | cbvabdavw 36257* | Change bound variable in class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑦 ∣ 𝜒}) | ||
| Theorem | cbvsbcdavw 36258* | Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑦]𝜒)) | ||
| Theorem | cbvsbcdavw2 36259* | Change bound variable of a class substitution. General version of cbvsbcdavw 36258. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑦]𝜒)) | ||
| Theorem | cbvcsbdavw 36260* | Change bound variable of a proper substitution into a class. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶) | ||
| Theorem | cbvcsbdavw2 36261* | Change bound variable of a proper substitution into a class. General version of cbvcsbdavw 36260. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷) | ||
| Theorem | cbvrabdavw 36262* | Change bound variable in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐴 ∣ 𝜒}) | ||
| Theorem | cbviundavw 36263* | Change bound variable in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶) | ||
| Theorem | cbviindavw 36264* | Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶) | ||
| Theorem | cbvopab1davw 36265* | Change the first bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑧, 𝑦〉 ∣ 𝜒}) | ||
| Theorem | cbvopab2davw 36266* | Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑧〉 ∣ 𝜒}) | ||
| Theorem | cbvopabdavw 36267* | Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑧, 𝑤〉 ∣ 𝜒}) | ||
| Theorem | cbvmptdavw 36268* | Change bound variable in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)) | ||
| Theorem | cbvdisjdavw 36269* | Change bound variable in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)) | ||
| Theorem | cbviotadavw 36270* | Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑦𝜒)) | ||
| Theorem | cbvriotadavw 36271* | Change bound variable in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐴 𝜒)) | ||
| Theorem | cbvoprab1davw 36272* | Change the first bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑧〉 ∣ 𝜒}) | ||
| Theorem | cbvoprab2davw 36273* | Change the second bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑧〉 ∣ 𝜒}) | ||
| Theorem | cbvoprab3davw 36274* | Change the third bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑧 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ 𝜒}) | ||
| Theorem | cbvoprab123davw 36275* | Change all bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑢〉, 𝑣〉 ∣ 𝜒}) | ||
| Theorem | cbvoprab12davw 36276* | Change the first and second bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑣〉, 𝑧〉 ∣ 𝜒}) | ||
| Theorem | cbvoprab23davw 36277* | Change the second and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (((𝜑 ∧ 𝑦 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑣〉 ∣ 𝜒}) | ||
| Theorem | cbvoprab13davw 36278* | Change the first and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑣〉 ∣ 𝜒}) | ||
| Theorem | cbvixpdavw 36279* | Change bound variable in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶) | ||
| Theorem | cbvsumdavw 36280* | Change bound variable in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑘 = 𝑗) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑗 ∈ 𝐴 𝐶) | ||
| Theorem | cbvproddavw 36281* | Change bound variable in a product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
| Theorem | cbvitgdavw 36282* | Change bound variable in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦) | ||
| Theorem | cbvditgdavw 36283* | Change bound variable in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦) | ||
| Theorem | cbvrmodavw2 36284* | Change bound variable and quantifier domain in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐵 𝜒)) | ||
| Theorem | cbvreudavw2 36285* | Change bound variable and quantifier domain in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐵 𝜒)) | ||
| Theorem | cbvrabdavw2 36286* | Change bound variable and domain in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
| Theorem | cbviundavw2 36287* | Change bound variable and domain in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷) | ||
| Theorem | cbviindavw2 36288* | Change bound variable and domain in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷) | ||
| Theorem | cbvmptdavw2 36289* | Change bound variable and domain in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷)) | ||
| Theorem | cbvdisjdavw2 36290* | Change bound variable and domain in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷)) | ||
| Theorem | cbvriotadavw2 36291* | Change bound variable and domain in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐵 𝜒)) | ||
| Theorem | cbvmpodavw2 36292* | Change bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹) & ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) & ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹)) | ||
| Theorem | cbvmpo1davw2 36293* | Change first bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐸 = 𝐹) & ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)) | ||
| Theorem | cbvmpo2davw2 36294* | Change second bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐸 = 𝐹) & ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹)) | ||
| Theorem | cbvixpdavw2 36295* | Change bound variable and domain in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷) | ||
| Theorem | cbvsumdavw2 36296* | Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | cbvproddavw2 36297* | Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | cbvitgdavw2 36298* | Change bound variable and domain in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦) | ||
| Theorem | cbvditgdavw2 36299* | Change bound variable and limits in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦) | ||
| Theorem | mpomulnzcnf 36300* | Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf 11909 using maps-to notation, which does not require ax-mulf 11235. (Contributed by GG, 18-Apr-2025.) |
| ⊢ (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · 𝑦)):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |