P. 368 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ditgeq3sdv 36701*	Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
21.12.2  Change bound variables
Theorem	in-ax8 36702	A proof of ax-8 2143 that does not rely on ax-8 2143. It employs df-in 3911 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2151. 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 36703	A proof of ax-8 2143 that does not rely on ax-8 2143. It employs df-ss 3921 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2151. Contrary to in-ax8 36702, this proof does not rely on df-cleq 2753, 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.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
21.12.2.1  Change bound variables and domains
Theorem	cbvralvw2 36704*	Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexvw2 36705*	Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrmovw2 36706*	Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreuvw2 36707*	Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvsbcvw2 36708*	Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3777. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓)
Theorem	cbvcsbvw2 36709*	Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv 3864. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷
Theorem	cbviunvw2 36710*	Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷
Theorem	cbviinvw2 36711*	Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷
Theorem	cbvmptvw2 36712*	Change bound variable and domain in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvdisjvw2 36713*	Change bound variable and domain in a disjoint collection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷)
Theorem	cbvriotavw2 36714*	Change bound variable and domain in a restricted description binder, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐵 𝜓)
Theorem	cbvoprab1vw 36715*	Change the first bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab2vw 36716*	Change the second bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab123vw 36717*	Change all bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab23vw 36718*	Change the second and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab13vw 36719*	Change the first and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvmpovw2 36720*	Change bound variables and domains in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo1vw2 36721*	Change domains and the first bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo2vw2 36722*	Change domains and the second bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvixpvw2 36723*	Change bound variable and domain in an indexed Cartesian product, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷
Theorem	cbvsumvw2 36724*	Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷
Theorem	cbvprodvw2 36725*	Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷
Theorem	cbvitgvw2 36726*	Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦
Theorem	cbvditgvw2 36727*	Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹)    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦
21.12.2.2  Change bound variables, deduction versions
Theorem	cbvmodavw 36728*	Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑦𝜒))
Theorem	cbveudavw 36729*	Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))
Theorem	cbvrmodavw 36730*	Change bound variable in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐴 𝜒))
Theorem	cbvreudavw 36731*	Change bound variable in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))
Theorem	cbvsbdavw 36732*	Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑦]𝜒))
Theorem	cbvsbdavw2 36733*	Change bound variable in proper substitution. General version of cbvsbdavw 36732. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝑧 = 𝑤)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑤 / 𝑦]𝜒))
Theorem	cbvabdavw 36734*	Change bound variable in class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑦 ∣ 𝜒})
Theorem	cbvsbcdavw 36735*	Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑦]𝜒))
Theorem	cbvsbcdavw2 36736*	Change bound variable of a class substitution. General version of cbvsbcdavw 36735. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑦]𝜒))
Theorem	cbvcsbdavw 36737*	Change bound variable of a proper substitution into a class. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶)
Theorem	cbvcsbdavw2 36738*	Change bound variable of a proper substitution into a class. General version of cbvcsbdavw 36737. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷)
Theorem	cbvrabdavw 36739*	Change bound variable in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐴 ∣ 𝜒})
Theorem	cbviundavw 36740*	Change bound variable in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbviindavw 36741*	Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvopab1davw 36742*	Change the first bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑦⟩ ∣ 𝜒})
Theorem	cbvopab2davw 36743*	Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑧⟩ ∣ 𝜒})
Theorem	cbvopabdavw 36744*	Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑤⟩ ∣ 𝜒})
Theorem	cbvmptdavw 36745*	Change bound variable in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶))
Theorem	cbvdisjdavw 36746*	Change bound variable in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶))
Theorem	cbviotadavw 36747*	Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑦𝜒))
Theorem	cbvriotadavw 36748*	Change bound variable in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐴 𝜒))
Theorem	cbvoprab1davw 36749*	Change the first bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab2davw 36750*	Change the second bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab3davw 36751*	Change the third bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑧 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜒})
Theorem	cbvoprab123davw 36752*	Change all bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab12davw 36753*	Change the first and second bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab23davw 36754*	Change the second and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑦 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab13davw 36755*	Change the first and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvixpdavw 36756*	Change bound variable in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶)
Theorem	cbvsumdavw 36757*	Change bound variable in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑘 = 𝑗) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑗 ∈ 𝐴 𝐶)
Theorem	cbvproddavw 36758*	Change bound variable in a product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	cbvitgdavw 36759*	Change bound variable in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦)
Theorem	cbvditgdavw 36760*	Change bound variable in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦)
21.12.2.3  Change bound variables and domains, deduction versions
Theorem	cbvrmodavw2 36761*	Change bound variable and quantifier domain in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐵 𝜒))
Theorem	cbvreudavw2 36762*	Change bound variable and quantifier domain in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐵 𝜒))
Theorem	cbvrabdavw2 36763*	Change bound variable and domain in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐵 ∣ 𝜒})
Theorem	cbviundavw2 36764*	Change bound variable and domain in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	cbviindavw2 36765*	Change bound variable and domain in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷)
Theorem	cbvmptdavw2 36766*	Change bound variable and domain in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	cbvdisjdavw2 36767*	Change bound variable and domain in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷))
Theorem	cbvriotadavw2 36768*	Change bound variable and domain in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐵 𝜒))
Theorem	cbvmpodavw2 36769*	Change bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹)    &   ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    &   ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvmpo1davw2 36770*	Change first bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐸 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvmpo2davw2 36771*	Change second bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐸 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvixpdavw2 36772*	Change bound variable and domain in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷)
Theorem	cbvsumdavw2 36773*	Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	cbvproddavw2 36774*	Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	cbvitgdavw2 36775*	Change bound variable and domain in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦)
Theorem	cbvditgdavw2 36776*	Change bound variable and limits in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦)
21.12.3  Study of ax-mulf usage
Theorem	mpomulnzcnf 36777*	Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf 11859 using maps-to notation, which does not require ax-mulf 11179. (Contributed by GG, 18-Apr-2025.)
⊢ (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · 𝑦)):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0})
21.13  Mathbox for Jeff Hankins
21.13.1  Miscellany
Theorem	a1i14 36778	Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.)
⊢ (𝜓 → (𝜒 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	a1i24 36779	Add two antecedents to a wff. Deduction associated with a1i13 28. (Contributed by Jeff Hankins, 5-Aug-2009.)
⊢ (𝜑 → (𝜒 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp5d 36780	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5g 36781	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5k 36782	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp56 36783	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp58 36784	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ ((𝜒 ∧ 𝜃) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp510 36785	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ (((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp511 36786	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp512 36787	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏))) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	3com12d 36788	Commutation in consequent. Swap 1st and 2nd. (Contributed by Jeff Hankins, 17-Nov-2009.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	imp5p 36789	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)))
Theorem	imp5q 36790	A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂))
Theorem	subtr 36791	Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝑌    &   ⊢ Ⅎ𝑥𝑍    &   ⊢ (𝑥 = 𝐴 → 𝑋 = 𝑌)    &   ⊢ (𝑥 = 𝐵 → 𝑋 = 𝑍)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → 𝑌 = 𝑍))
Theorem	subtr2 36792	Transitivity of implicit substitution into a wff. (Contributed by Jeff Hankins, 19-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 = 𝐵 → (𝜓 ↔ 𝜒)))
Theorem	trer 36793*	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 36794	An equivalent membership condition for closed intervals. (Contributed by Jeff Hankins, 14-Jul-2009.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ∧ (𝐶 = 𝐴 ∨ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ∨ 𝐶 = 𝐵))))
Theorem	finminlem 36795*	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 𝜑 → ∃𝑥(𝜑 ∧ ∀𝑦((𝑦 ⊆ 𝑥 ∧ 𝜓) → 𝑥 = 𝑦)))
Theorem	gtinf 36796*	Any number greater than an infimum is greater than some element of the set. (Contributed by Jeff Hankins, 29-Sep-2013.) (Revised by AV, 10-Oct-2021.)
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦) ∧ (𝐴 ∈ ℝ ∧ inf(𝑆, ℝ, < ) < 𝐴)) → ∃𝑧 ∈ 𝑆 𝑧 < 𝐴)
Theorem	opnrebl 36797*	A set is open in the standard topology of the reals precisely when every point can be enclosed in an open ball. (Contributed by Jeff Hankins, 23-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐴 ∈ (topGen‘ran (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ℝ+ ((𝑥 − 𝑦)(,)(𝑥 + 𝑦)) ⊆ 𝐴))
Theorem	opnrebl2 36798*	A set is open in the standard topology of the reals precisely when every point can be enclosed in an arbitrarily small ball. (Contributed by Jeff Hankins, 22-Sep-2013.) (Proof shortened by Mario Carneiro, 30-Jan-2014.)
⊢ (𝐴 ∈ (topGen‘ran (,)) ↔ (𝐴 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ (𝑧 ≤ 𝑦 ∧ ((𝑥 − 𝑧)(,)(𝑥 + 𝑧)) ⊆ 𝐴)))
Theorem	nn0prpwlem 36799*	Lemma for nn0prpw 36800. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.)
⊢ (𝐴 ∈ ℕ → ∀𝑘 ∈ ℕ (𝑘 < 𝐴 → ∃𝑝 ∈ ℙ ∃𝑛 ∈ ℕ ¬ ((𝑝↑𝑛) ∥ 𝑘 ↔ (𝑝↑𝑛) ∥ 𝐴)))
Theorem	nn0prpw 36800*	Two nonnegative integers are the same if and only if they are divisible by the same prime powers. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ((𝑝↑𝑛) ∥ 𝐴 ↔ (𝑝↑𝑛) ∥ 𝐵)))