![]() |
Metamath
Proof Explorer Theorem List (p. 363 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | itgeq12sdv 36201* | Equality theorem for an integral. Deduction form. General version of itgeq1d 45912 and itgeq2sdv 36202. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥) | ||
Theorem | itgeq2sdv 36202* | Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥) | ||
Theorem | ditgeq123dv 36203* | Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv 36205. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ (𝜑 → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥) | ||
Theorem | ditgeq12d 36204* | Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥) | ||
Theorem | ditgeq3sdv 36205* | Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.) |
⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥) | ||
Theorem | in-ax8 36206 | A proof of ax-8 2107 that does not rely on ax-8 2107. It employs df-in 3969 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2115. 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 36207 | A proof of ax-8 2107 that does not rely on ax-8 2107. It employs df-ss 3979 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2115. Contrary to in-ax8 36206, this proof does not rely on df-cleq 2726, 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 36208* | Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrexvw2 36209* | Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvrmovw2 36210* | Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvreuvw2 36211* | Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvsbcvw2 36212* | Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3825. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓) | ||
Theorem | cbvcsbvw2 36213* | Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv 3919. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷 | ||
Theorem | cbviunvw2 36214* | Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷 | ||
Theorem | cbviinvw2 36215* | Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷 | ||
Theorem | cbvmptvw2 36216* | Change bound variable and domain in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | cbvdisjvw2 36217* | Change bound variable and domain in a disjoint collection, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷) | ||
Theorem | cbvriotavw2 36218* | Change bound variable and domain in a restricted description binder, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐵 𝜓) | ||
Theorem | cbvoprab1vw 36219* | Change the first bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑤 → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑧〉 ∣ 𝜒} | ||
Theorem | cbvoprab2vw 36220* | Change the second bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑧〉 ∣ 𝜒} | ||
Theorem | cbvoprab123vw 36221* | Change all bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑢〉, 𝑣〉 ∣ 𝜒} | ||
Theorem | cbvoprab23vw 36222* | Change the second and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑣〉 ∣ 𝜒} | ||
Theorem | cbvoprab13vw 36223* | Change the first and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝑥 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑣〉 ∣ 𝜒} | ||
Theorem | cbvmpovw2 36224* | Change bound variables and domains in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹) & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹) | ||
Theorem | cbvmpo1vw2 36225* | Change domains and the first bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑧 → 𝐸 = 𝐹) & ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑧 → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹) | ||
Theorem | cbvmpo2vw2 36226* | Change domains and the second bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑦 = 𝑧 → 𝐸 = 𝐹) & ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷) & ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐵) ⇒ ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹) | ||
Theorem | cbvixpvw2 36227* | Change bound variable and domain in an indexed Cartesian product, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷 | ||
Theorem | cbvsumvw2 36228* | Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷) ⇒ ⊢ Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷 | ||
Theorem | cbvprodvw2 36229* | Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷) ⇒ ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷 | ||
Theorem | cbvitgvw2 36230* | Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦 | ||
Theorem | cbvditgvw2 36231* | Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 & ⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹) ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦 | ||
Theorem | cbvmodavw 36232* | Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑦𝜒)) | ||
Theorem | cbveudavw 36233* | Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒)) | ||
Theorem | cbvrmodavw 36234* | Change bound variable in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvreudavw 36235* | Change bound variable in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvsbdavw 36236* | Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑦]𝜒)) | ||
Theorem | cbvsbdavw2 36237* | Change bound variable in proper substitution. General version of cbvsbdavw 36236. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝜑 → 𝑧 = 𝑤) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑤 / 𝑦]𝜒)) | ||
Theorem | cbvabdavw 36238* | Change bound variable in class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑦 ∣ 𝜒}) | ||
Theorem | cbvsbcdavw 36239* | Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑦]𝜒)) | ||
Theorem | cbvsbcdavw2 36240* | Change bound variable of a class substitution. General version of cbvsbcdavw 36239. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑦]𝜒)) | ||
Theorem | cbvcsbdavw 36241* | Change bound variable of a proper substitution into a class. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶) | ||
Theorem | cbvcsbdavw2 36242* | Change bound variable of a proper substitution into a class. General version of cbvcsbdavw 36241. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷) | ||
Theorem | cbvrabdavw 36243* | Change bound variable in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐴 ∣ 𝜒}) | ||
Theorem | cbviundavw 36244* | Change bound variable in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | cbviindavw 36245* | Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶) | ||
Theorem | cbvopab1davw 36246* | Change the first bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑧, 𝑦〉 ∣ 𝜒}) | ||
Theorem | cbvopab2davw 36247* | Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑧〉 ∣ 𝜒}) | ||
Theorem | cbvopabdavw 36248* | Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑧, 𝑤〉 ∣ 𝜒}) | ||
Theorem | cbvmptdavw 36249* | Change bound variable in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)) | ||
Theorem | cbvdisjdavw 36250* | Change bound variable in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶)) | ||
Theorem | cbviotadavw 36251* | Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑦𝜒)) | ||
Theorem | cbvriotadavw 36252* | Change bound variable in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐴 𝜒)) | ||
Theorem | cbvoprab1davw 36253* | Change the first bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑧〉 ∣ 𝜒}) | ||
Theorem | cbvoprab2davw 36254* | Change the second bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑧〉 ∣ 𝜒}) | ||
Theorem | cbvoprab3davw 36255* | Change the third bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑧 = 𝑤) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ 𝜒}) | ||
Theorem | cbvoprab123davw 36256* | Change all bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑢〉, 𝑣〉 ∣ 𝜒}) | ||
Theorem | cbvoprab12davw 36257* | Change the first and second bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑣〉, 𝑧〉 ∣ 𝜒}) | ||
Theorem | cbvoprab23davw 36258* | Change the second and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (((𝜑 ∧ 𝑦 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑥, 𝑤〉, 𝑣〉 ∣ 𝜒}) | ||
Theorem | cbvoprab13davw 36259* | Change the first and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜓} = {〈〈𝑤, 𝑦〉, 𝑣〉 ∣ 𝜒}) | ||
Theorem | cbvixpdavw 36260* | Change bound variable in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶) | ||
Theorem | cbvsumdavw 36261* | Change bound variable in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑘 = 𝑗) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑗 ∈ 𝐴 𝐶) | ||
Theorem | cbvproddavw 36262* | Change bound variable in a product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶) | ||
Theorem | cbvitgdavw 36263* | Change bound variable in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦) | ||
Theorem | cbvditgdavw 36264* | Change bound variable in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦) | ||
Theorem | cbvrmodavw2 36265* | Change bound variable and quantifier domain in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvreudavw2 36266* | Change bound variable and quantifier domain in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvrabdavw2 36267* | Change bound variable and domain in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | cbviundavw2 36268* | Change bound variable and domain in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷) | ||
Theorem | cbviindavw2 36269* | Change bound variable and domain in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷) | ||
Theorem | cbvmptdavw2 36270* | Change bound variable and domain in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷)) | ||
Theorem | cbvdisjdavw2 36271* | Change bound variable and domain in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷)) | ||
Theorem | cbvriotadavw2 36272* | Change bound variable and domain in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | cbvmpodavw2 36273* | Change bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹) & ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) & ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹)) | ||
Theorem | cbvmpo1davw2 36274* | Change first bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐸 = 𝐹) & ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)) | ||
Theorem | cbvmpo2davw2 36275* | Change second bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐸 = 𝐹) & ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹)) | ||
Theorem | cbvixpdavw2 36276* | Change bound variable and domain in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷) | ||
Theorem | cbvsumdavw2 36277* | Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) | ||
Theorem | cbvproddavw2 36278* | Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
Theorem | cbvitgdavw2 36279* | Change bound variable and domain in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦) | ||
Theorem | cbvditgdavw2 36280* | Change bound variable and limits in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) & ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐸 = 𝐹) ⇒ ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦) | ||
Theorem | mpomulnzcnf 36281* | Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf 11906 using maps-to notation, which does not require ax-mulf 11232. (Contributed by GG, 18-Apr-2025.) |
⊢ (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · 𝑦)):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0}) | ||
Theorem | a1i14 36282 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
⊢ (𝜓 → (𝜒 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | a1i24 36283 | Add two antecedents to a wff. Deduction associated with a1i13 27. (Contributed by Jeff Hankins, 5-Aug-2009.) |
⊢ (𝜑 → (𝜒 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp5d 36284 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp5g 36285 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp5k 36286 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → (((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp56 36287 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp58 36288 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (((𝜑 ∧ 𝜓) ∧ ((𝜒 ∧ 𝜃) ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp510 36289 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ ((𝜑 ∧ (((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp511 36290 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp512 36291 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏))) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | 3com12d 36292 | Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | imp5p 36293 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂))) | ||
Theorem | imp5q 36294 | A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)) | ||
Theorem | ecase13d 36295 | Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → ¬ 𝜃) & ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | subtr 36296 | Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑌 & ⊢ Ⅎ𝑥𝑍 & ⊢ (𝑥 = 𝐴 → 𝑋 = 𝑌) & ⊢ (𝑥 = 𝐵 → 𝑋 = 𝑍) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → 𝑌 = 𝑍)) | ||
Theorem | subtr2 36297 | Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → (𝜓 ↔ 𝜒))) | ||
Theorem | trer 36298* | A relation intersected with its converse is an equivalence relation if the relation is transitive. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ )) | ||
Theorem | elicc3 36299 | An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ (𝐶 = 𝐴 ∨ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ∨ 𝐶 = 𝐵)))) | ||
Theorem | finminlem 36300* | A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. (Contributed by Jeff Hankins, 4-Dec-2009.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥 ∈ Fin 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |