P. 373 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37201-37300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prodeq2si 37201	Equality inference for product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq12si 37202	Equality inference for product. General version of prodeq2si 37201. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷
Theorem	itgeq12i 37203	Equality inference for an integral. General version of itgeq1i 37204 and itgeq2i 37205. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥
Theorem	itgeq1i 37204	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥
Theorem	itgeq2i 37205	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥
Theorem	ditgeq123i 37206	Equality inference for the directed integral. General version of ditgeq12i 37207 and ditgeq3i 37208. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ 𝐸 = 𝐹    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥
Theorem	ditgeq12i 37207	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥
Theorem	ditgeq3i 37208	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥
21.13.1.2  Deduction versions
Theorem	rmoeqdv 37209*	Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	rmoeqbidv 37210*	Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3384. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒))
Theorem	sbequbidv 37211*	Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝑢 = 𝑣)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒))
Theorem	disjeq12dv 37212*	Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	ixpeq12dv 37213*	Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷)
Theorem	sumeq12sdv 37214*	Equality deduction for sum. General version of sumeq2sdv 15911. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	prodeq12sdv 37215*	Equality deduction for product. General version of prodeq2sdv 16132. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	itgeq12sdv 37216*	Equality theorem for an integral. Deduction form. General version of itgeq1d 47234 and itgeq2sdv 37217. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥)
Theorem	itgeq2sdv 37217*	Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	ditgeq123dv 37218*	Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv 37220. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥)
Theorem	ditgeq12d 37219*	Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥)
Theorem	ditgeq3sdv 37220*	Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥)
21.13.2  Change bound variables
Theorem	in-ax8 37221	A proof of ax-8 2149 that does not rely on ax-8 2149. It employs df-in 4094 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2157. 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 37222	A proof of ax-8 2149 that does not rely on ax-8 2149. It employs df-ss 3901 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2157. Contrary to in-ax8 37221, this proof does not rely on df-cleq 2755, 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.13.2.1  Change bound variables and domains
Theorem	cbvralvw2 37223*	Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexvw2 37224*	Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrmovw2 37225*	Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreuvw2 37226*	Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvsbcvw2 37227*	Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3776. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓)
Theorem	cbvcsbvw2 37228*	Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv 3863. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷
Theorem	cbviunvw2 37229*	Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷
Theorem	cbviinvw2 37230*	Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷
Theorem	cbvmptvw2 37231*	Change bound variable and domain in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvdisjvw2 37232*	Change bound variable and domain in a disjoint collection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷)
Theorem	cbvriotavw2 37233*	Change bound variable and domain in a restricted description binder, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐵 𝜓)
Theorem	cbvoprab1vw 37234*	Change the first bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab2vw 37235*	Change the second bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab123vw 37236*	Change all bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab23vw 37237*	Change the second and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab13vw 37238*	Change the first and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvmpovw2 37239*	Change bound variables and domains in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo1vw2 37240*	Change domains and the first bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo2vw2 37241*	Change domains and the second bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvixpvw2 37242*	Change bound variable and domain in an indexed Cartesian product, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷
Theorem	cbvsumvw2 37243*	Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷
Theorem	cbvprodvw2 37244*	Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷
Theorem	cbvitgvw2 37245*	Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦
Theorem	cbvditgvw2 37246*	Change bound variable and domain in a directed integral, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹)    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦
21.13.2.2  Change bound variables, deduction versions
Theorem	cbvmodavw 37247*	Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑦𝜒))
Theorem	cbveudavw 37248*	Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))
Theorem	cbvrmodavw 37249*	Change bound variable in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐴 𝜒))
Theorem	cbvreudavw 37250*	Change bound variable in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))
Theorem	cbvsbdavw 37251*	Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑦]𝜒))
Theorem	cbvsbdavw2 37252*	Change bound variable in proper substitution. General version of cbvsbdavw 37251. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝑧 = 𝑤)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑤 / 𝑦]𝜒))
Theorem	cbvabdavw 37253*	Change bound variable in class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑦 ∣ 𝜒})
Theorem	cbvsbcdavw 37254*	Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑦]𝜒))
Theorem	cbvsbcdavw2 37255*	Change bound variable of a class substitution. General version of cbvsbcdavw 37254. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑦]𝜒))
Theorem	cbvcsbdavw 37256*	Change bound variable of a proper substitution into a class. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶)
Theorem	cbvcsbdavw2 37257*	Change bound variable of a proper substitution into a class. General version of cbvcsbdavw 37256. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷)
Theorem	cbvrabdavw 37258*	Change bound variable in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐴 ∣ 𝜒})
Theorem	cbviundavw 37259*	Change bound variable in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbviindavw 37260*	Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvopab1davw 37261*	Change the first bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑦⟩ ∣ 𝜒})
Theorem	cbvopab2davw 37262*	Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑧⟩ ∣ 𝜒})
Theorem	cbvopabdavw 37263*	Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑤⟩ ∣ 𝜒})
Theorem	cbvmptdavw 37264*	Change bound variable in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶))
Theorem	cbvdisjdavw 37265*	Change bound variable in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶))
Theorem	cbviotadavw 37266*	Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑦𝜒))
Theorem	cbvriotadavw 37267*	Change bound variable in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐴 𝜒))
Theorem	cbvoprab1davw 37268*	Change the first bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab2davw 37269*	Change the second bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab3davw 37270*	Change the third bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑧 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜒})
Theorem	cbvoprab123davw 37271*	Change all bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab12davw 37272*	Change the first and second bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab23davw 37273*	Change the second and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑦 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab13davw 37274*	Change the first and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvixpdavw 37275*	Change bound variable in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶)
Theorem	cbvsumdavw 37276*	Change bound variable in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑘 = 𝑗) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑗 ∈ 𝐴 𝐶)
Theorem	cbvproddavw 37277*	Change bound variable in a product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)
Theorem	cbvitgdavw 37278*	Change bound variable in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦)
Theorem	cbvditgdavw 37279*	Change bound variable in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦)
21.13.2.3  Change bound variables and domains, deduction versions
Theorem	cbvrmodavw2 37280*	Change bound variable and quantifier domain in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐵 𝜒))
Theorem	cbvreudavw2 37281*	Change bound variable and quantifier domain in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐵 𝜒))
Theorem	cbvrabdavw2 37282*	Change bound variable and domain in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐵 ∣ 𝜒})
Theorem	cbviundavw2 37283*	Change bound variable and domain in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷)
Theorem	cbviindavw2 37284*	Change bound variable and domain in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷)
Theorem	cbvmptdavw2 37285*	Change bound variable and domain in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷))
Theorem	cbvdisjdavw2 37286*	Change bound variable and domain in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷))
Theorem	cbvriotadavw2 37287*	Change bound variable and domain in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐵 𝜒))
Theorem	cbvmpodavw2 37288*	Change bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹)    &   ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    &   ⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvmpo1davw2 37289*	Change first bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐸 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvmpo2davw2 37290*	Change second bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐸 = 𝐹)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 = 𝑧) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹))
Theorem	cbvixpdavw2 37291*	Change bound variable and domain in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷)
Theorem	cbvsumdavw2 37292*	Change bound variable and the set of integers in a sum. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	cbvproddavw2 37293*	Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑗 = 𝑘) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	cbvitgdavw2 37294*	Change bound variable and domain in an integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦)
Theorem	cbvditgdavw2 37295*	Change bound variable and limits in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑦)
21.13.3  Study of ax-mulf usage
Theorem	mpomulnzcnf 37296*	Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf 12000 using maps-to notation, which does not require ax-mulf 11317. (Contributed by GG, 18-Apr-2025.)
⊢ (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · 𝑦)):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0})
21.14  Mathbox for Jeff Hankins
21.14.1  Miscellany
Theorem	a1i14 37297	Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.)
⊢ (𝜓 → (𝜒 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	a1i24 37298	Add two antecedents to a wff. Deduction associated with a1i13 28. (Contributed by Jeff Hankins, 5-Aug-2009.)
⊢ (𝜑 → (𝜒 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp5d 37299	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5g 37300	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))