P. 365 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36401-36500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hfsn 36401	The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ Hf → {𝐴} ∈ Hf )
Theorem	hfadj 36402	Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ {𝐵}) ∈ Hf )
Theorem	hfelhf 36403	Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ Hf ) → 𝐴 ∈ Hf )
Theorem	hftr 36404	The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ Tr Hf
Theorem	hfext 36405*	Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ Hf (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
Theorem	hfuni 36406	The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf )
Theorem	hfpw 36407	The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf )
Theorem	hfninf 36408	ω is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ¬ ω ∈ Hf
21.12  Mathbox for Gino Giotto
21.12.1  Equality theorems
21.12.1.1  Inference versions
Theorem	rmoeqi 36409	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)
Theorem	rmoeqbii 36410	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)
Theorem	reueqi 36411	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	reueqbii 36412	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒)
Theorem	sbceqbii 36413	Formula-building inference for class substitution. General version of sbcbii 3799. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓)
Theorem	disjeq1i 36414	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)
Theorem	disjeq12i 36415	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)
Theorem	rabeqbii 36416	Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓}
Theorem	iuneq12i 36417	Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷
Theorem	iineq1i 36418	Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶
Theorem	iineq12i 36419	Equality theorem for indexed intersection. Inference version. General version of iineq1i 36418. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷
Theorem	riotaeqbii 36420	Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓)
Theorem	riotaeqi 36421	Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)
Theorem	ixpeq1i 36422	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶
Theorem	ixpeq12i 36423	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷
Theorem	sumeq2si 36424	Equality inference for sum. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq12si 36425	Equality inference for sum. General version of sumeq2si 36424. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷
Theorem	prodeq2si 36426	Equality inference for product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq12si 36427	Equality inference for product. General version of prodeq2si 36426. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷
Theorem	itgeq12i 36428	Equality inference for an integral. General version of itgeq1i 36429 and itgeq2i 36430. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥
Theorem	itgeq1i 36429	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥
Theorem	itgeq2i 36430	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥
Theorem	ditgeq123i 36431	Equality inference for the directed integral. General version of ditgeq12i 36432 and ditgeq3i 36433. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ 𝐸 = 𝐹    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥
Theorem	ditgeq12i 36432	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥
Theorem	ditgeq3i 36433	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥
21.12.1.2  Deduction versions
Theorem	rmoeqdv 36434*	Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	rmoeqbidv 36435*	Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3367. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒))
Theorem	sbequbidv 36436*	Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝑢 = 𝑣)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒))
Theorem	disjeq12dv 36437*	Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	ixpeq12dv 36438*	Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷)
Theorem	sumeq12sdv 36439*	Equality deduction for sum. General version of sumeq2sdv 15640. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	prodeq12sdv 36440*	Equality deduction for product. General version of prodeq2sdv 15860. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	itgeq12sdv 36441*	Equality theorem for an integral. Deduction form. General version of itgeq1d 46344 and itgeq2sdv 36442. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥)
Theorem	itgeq2sdv 36442*	Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	ditgeq123dv 36443*	Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv 36445. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥)
Theorem	ditgeq12d 36444*	Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥)
Theorem	ditgeq3sdv 36445*	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 36446	A proof of ax-8 2116 that does not rely on ax-8 2116. It employs df-in 3910 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2124. 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 36447	A proof of ax-8 2116 that does not rely on ax-8 2116. It employs df-ss 3920 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2124. Contrary to in-ax8 36446, 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.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
21.12.2.1  Change bound variables and domains
Theorem	cbvralvw2 36448*	Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexvw2 36449*	Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrmovw2 36450*	Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreuvw2 36451*	Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvsbcvw2 36452*	Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3776. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓)
Theorem	cbvcsbvw2 36453*	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 36454*	Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷
Theorem	cbviinvw2 36455*	Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷
Theorem	cbvmptvw2 36456*	Change bound variable and domain in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvdisjvw2 36457*	Change bound variable and domain in a disjoint collection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷)
Theorem	cbvriotavw2 36458*	Change bound variable and domain in a restricted description binder, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐵 𝜓)
Theorem	cbvoprab1vw 36459*	Change the first bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab2vw 36460*	Change the second bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab123vw 36461*	Change all bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab23vw 36462*	Change the second and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab13vw 36463*	Change the first and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvmpovw2 36464*	Change bound variables and domains in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo1vw2 36465*	Change domains and the first bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo2vw2 36466*	Change domains and the second bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvixpvw2 36467*	Change bound variable and domain in an indexed Cartesian product, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷
Theorem	cbvsumvw2 36468*	Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷
Theorem	cbvprodvw2 36469*	Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷
Theorem	cbvitgvw2 36470*	Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦
Theorem	cbvditgvw2 36471*	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 36472*	Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑦𝜒))
Theorem	cbveudavw 36473*	Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))
Theorem	cbvrmodavw 36474*	Change bound variable in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐴 𝜒))
Theorem	cbvreudavw 36475*	Change bound variable in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))
Theorem	cbvsbdavw 36476*	Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑦]𝜒))
Theorem	cbvsbdavw2 36477*	Change bound variable in proper substitution. General version of cbvsbdavw 36476. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝑧 = 𝑤)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑤 / 𝑦]𝜒))
Theorem	cbvabdavw 36478*	Change bound variable in class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑦 ∣ 𝜒})
Theorem	cbvsbcdavw 36479*	Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑦]𝜒))
Theorem	cbvsbcdavw2 36480*	Change bound variable of a class substitution. General version of cbvsbcdavw 36479. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑦]𝜒))
Theorem	cbvcsbdavw 36481*	Change bound variable of a proper substitution into a class. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶)
Theorem	cbvcsbdavw2 36482*	Change bound variable of a proper substitution into a class. General version of cbvcsbdavw 36481. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷)
Theorem	cbvrabdavw 36483*	Change bound variable in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐴 ∣ 𝜒})
Theorem	cbviundavw 36484*	Change bound variable in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbviindavw 36485*	Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvopab1davw 36486*	Change the first bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑦⟩ ∣ 𝜒})
Theorem	cbvopab2davw 36487*	Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑧⟩ ∣ 𝜒})
Theorem	cbvopabdavw 36488*	Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑧) ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑤⟩ ∣ 𝜒})
Theorem	cbvmptdavw 36489*	Change bound variable in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶))
Theorem	cbvdisjdavw 36490*	Change bound variable in a disjoint collection. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 𝐶))
Theorem	cbviotadavw 36491*	Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑦𝜒))
Theorem	cbvriotadavw 36492*	Change bound variable in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑦 ∈ 𝐴 𝜒))
Theorem	cbvoprab1davw 36493*	Change the first bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab2davw 36494*	Change the second bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab3davw 36495*	Change the third bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑧 = 𝑤) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑦⟩, 𝑤⟩ ∣ 𝜒})
Theorem	cbvoprab123davw 36496*	Change all bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab12davw 36497*	Change the first and second bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑦 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑣⟩, 𝑧⟩ ∣ 𝜒})
Theorem	cbvoprab23davw 36498*	Change the second and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑦 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvoprab13davw 36499*	Change the first and third bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝜑 ∧ 𝑥 = 𝑤) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒})
Theorem	cbvixpdavw 36500*	Change bound variable in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶)