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
21.11.19  Rank theorems
Theorem	rankung 36401	The rank of the union of two sets. Closed form of rankun 9778. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵)))
Theorem	ranksng 36402	The rank of a singleton. Closed form of ranksn 9776. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (rank‘{𝐴}) = suc (rank‘𝐴))
Theorem	rankelg 36403	The membership relation is inherited by the rank function. Closed form of rankel 9761. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝐵) → (rank‘𝐴) ∈ (rank‘𝐵))
Theorem	rankpwg 36404	The rank of a power set. Closed form of rankpw 9765. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (rank‘𝒫 𝐴) = suc (rank‘𝐴))
Theorem	rank0 36405	The rank of the empty set is ∅. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ (rank‘∅) = ∅
Theorem	rankeq1o 36406	The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.)
⊢ ((rank‘𝐴) = 1o ↔ 𝐴 = {∅})
21.11.20  Hereditarily Finite Sets
Syntax	chf 36407	The constant Hf is a class.
class Hf
Definition	df-hf 36408	Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ Hf = ∪ (𝑅1 “ ω)
Theorem	elhf 36409*	Membership in the hereditarily finite sets. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ (𝐴 ∈ Hf ↔ ∃𝑥 ∈ ω 𝐴 ∈ (𝑅1‘𝑥))
Theorem	elhf2 36410	Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω)
Theorem	elhf2g 36411	Hereditarily finiteness via rank. Closed form of elhf2 36410. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Hf ↔ (rank‘𝐴) ∈ ω))
Theorem	0hf 36412	The empty set is a hereditarily finite set. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ ∅ ∈ Hf
Theorem	hfun 36413	The union of two HF sets is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ 𝐵) ∈ Hf )
Theorem	hfsn 36414	The singleton of an HF set is an HF set. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ (𝐴 ∈ Hf → {𝐴} ∈ Hf )
Theorem	hfadj 36415	Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 ∪ {𝐵}) ∈ Hf )
Theorem	hfelhf 36416	Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ Hf ) → 𝐴 ∈ Hf )
Theorem	hftr 36417	The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ Tr Hf
Theorem	hfext 36418*	Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ ((𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ Hf (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
Theorem	hfuni 36419	The union of an HF set is itself hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → ∪ 𝐴 ∈ Hf )
Theorem	hfpw 36420	The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.)
⊢ (𝐴 ∈ Hf → 𝒫 𝐴 ∈ Hf )
Theorem	hfninf 36421	ω 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 36422	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)
Theorem	rmoeqbii 36423	Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)
Theorem	reueqi 36424	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓)
Theorem	reueqbii 36425	Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒)
Theorem	sbceqbii 36426	Formula-building inference for class substitution. General version of sbcbii 3786. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓)
Theorem	disjeq1i 36427	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶)
Theorem	disjeq12i 36428	Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)
Theorem	rabeqbii 36429	Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓}
Theorem	iuneq12i 36430	Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷
Theorem	iineq1i 36431	Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶
Theorem	iineq12i 36432	Equality theorem for indexed intersection. Inference version. General version of iineq1i 36431. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷
Theorem	riotaeqbii 36433	Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓)
Theorem	riotaeqi 36434	Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑)
Theorem	ixpeq1i 36435	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶
Theorem	ixpeq12i 36436	Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷
Theorem	sumeq2si 36437	Equality inference for sum. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶
Theorem	sumeq12si 36438	Equality inference for sum. General version of sumeq2si 36437. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷
Theorem	prodeq2si 36439	Equality inference for product. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶
Theorem	prodeq12si 36440	Equality inference for product. General version of prodeq2si 36439. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷
Theorem	itgeq12i 36441	Equality inference for an integral. General version of itgeq1i 36442 and itgeq2i 36443. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥
Theorem	itgeq1i 36442	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥
Theorem	itgeq2i 36443	Equality inference for an integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐵 = 𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥
Theorem	ditgeq123i 36444	Equality inference for the directed integral. General version of ditgeq12i 36445 and ditgeq3i 36446. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    &   ⊢ 𝐸 = 𝐹    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥
Theorem	ditgeq12i 36445	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥
Theorem	ditgeq3i 36446	Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐶 = 𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥
21.12.1.2  Deduction versions
Theorem	rmoeqdv 36447*	Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓))
Theorem	rmoeqbidv 36448*	Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3360. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒))
Theorem	sbequbidv 36449*	Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝑢 = 𝑣)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒))
Theorem	disjeq12dv 36450*	Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷))
Theorem	ixpeq12dv 36451*	Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷)
Theorem	sumeq12sdv 36452*	Equality deduction for sum. General version of sumeq2sdv 15663. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷)
Theorem	prodeq12sdv 36453*	Equality deduction for product. General version of prodeq2sdv 15886. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷)
Theorem	itgeq12sdv 36454*	Equality theorem for an integral. Deduction form. General version of itgeq1d 46407 and itgeq2sdv 36455. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥)
Theorem	itgeq2sdv 36455*	Equality theorem for an integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	ditgeq123dv 36456*	Equality theorem for the directed integral. Deduction form. General version of ditgeq3sdv 36458. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    &   ⊢ (𝜑 → 𝐸 = 𝐹)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥)
Theorem	ditgeq12d 36457*	Equality theorem for the directed integral. Deduction form. (Contributed by GG, 1-Sep-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥)
Theorem	ditgeq3sdv 36458*	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 36459	A proof of ax-8 2121 that does not rely on ax-8 2121. It employs df-in 3897 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2129. 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 36460	A proof of ax-8 2121 that does not rely on ax-8 2121. It employs df-ss 3907 to perform alpha-renaming and eliminates disjoint variable conditions using ax-9 2129. Contrary to in-ax8 36459, this proof does not rely on df-cleq 2732, 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 36461*	Change bound variable and domain in the restricted universal quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrexvw2 36462*	Change bound variable and domain in the restricted existential quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐵 𝜓)
Theorem	cbvrmovw2 36463*	Change bound variable and domain in the restricted at-most-one quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑦 ∈ 𝐵 𝜓)
Theorem	cbvreuvw2 36464*	Change bound variable and domain in the restricted existential uniqueness quantifier, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐵 𝜓)
Theorem	cbvsbcvw2 36465*	Change bound variable of a class substitution using implicit substitution. General version of cbvsbcvw 3764. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑦]𝜓)
Theorem	cbvcsbvw2 36466*	Change bound variable of a proper substitution into a class using implicit substitution. General version of cbvcsbv 3850. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷
Theorem	cbviunvw2 36467*	Change bound variable and domain in indexed unions, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑦 ∈ 𝐵 𝐷
Theorem	cbviinvw2 36468*	Change bound variable and domain in an indexed intersection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑦 ∈ 𝐵 𝐷
Theorem	cbvmptvw2 36469*	Change bound variable and domain in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑦 ∈ 𝐵 ↦ 𝐷)
Theorem	cbvdisjvw2 36470*	Change bound variable and domain in a disjoint collection, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑦 ∈ 𝐵 𝐷)
Theorem	cbvriotavw2 36471*	Change bound variable and domain in a restricted description binder, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐵 𝜓)
Theorem	cbvoprab1vw 36472*	Change the first bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab2vw 36473*	Change the second bound variable in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑧⟩ ∣ 𝜒}
Theorem	cbvoprab123vw 36474*	Change all bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑢⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab23vw 36475*	Change the second and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑥, 𝑤⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvoprab13vw 36476*	Change the first and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑤 ∧ 𝑧 = 𝑣) → (𝜓 ↔ 𝜒))    ⇒   ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜓} = {⟨⟨𝑤, 𝑦⟩, 𝑣⟩ ∣ 𝜒}
Theorem	cbvmpovw2 36477*	Change bound variables and domains in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐸 = 𝐹)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷)    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑤 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo1vw2 36478*	Change domains and the first bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑧 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvmpo2vw2 36479*	Change domains and the second bound variable in a maps-to function, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑦 = 𝑧 → 𝐸 = 𝐹)    &   ⊢ (𝑦 = 𝑧 → 𝐶 = 𝐷)    &   ⊢ (𝑦 = 𝑧 → 𝐴 = 𝐵)    ⇒   ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑧 ∈ 𝐷 ↦ 𝐹)
Theorem	cbvixpvw2 36480*	Change bound variable and domain in an indexed Cartesian product, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑦 ∈ 𝐵 𝐷
Theorem	cbvsumvw2 36481*	Change bound variable and the set of integers in a sum, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ Σ𝑗 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷
Theorem	cbvprodvw2 36482*	Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
⊢ 𝐴 = 𝐵    &   ⊢ (𝑗 = 𝑘 → 𝐶 = 𝐷)    ⇒   ⊢ ∏𝑗 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷
Theorem	cbvitgvw2 36483*	Change bound variable and domain in an integral, using implicit substitution. (Contributed by GG, 14-Aug-2025.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑦
Theorem	cbvditgvw2 36484*	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 36485*	Change bound variable in the at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑦𝜒))
Theorem	cbveudavw 36486*	Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑦𝜒))
Theorem	cbvrmodavw 36487*	Change bound variable in the restricted at-most-one quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑦 ∈ 𝐴 𝜒))
Theorem	cbvreudavw 36488*	Change bound variable in the restricted existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑦 ∈ 𝐴 𝜒))
Theorem	cbvsbdavw 36489*	Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑦]𝜒))
Theorem	cbvsbdavw2 36490*	Change bound variable in proper substitution. General version of cbvsbdavw 36489. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝑧 = 𝑤)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥]𝜓 ↔ [𝑤 / 𝑦]𝜒))
Theorem	cbvabdavw 36491*	Change bound variable in class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑦 ∣ 𝜒})
Theorem	cbvsbcdavw 36492*	Change bound variable of a class substitution. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐴 / 𝑦]𝜒))
Theorem	cbvsbcdavw2 36493*	Change bound variable of a class substitution. General version of cbvsbcdavw 36492. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑦]𝜒))
Theorem	cbvcsbdavw 36494*	Change bound variable of a proper substitution into a class. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑦⦌𝐶)
Theorem	cbvcsbdavw2 36495*	Change bound variable of a proper substitution into a class. General version of cbvcsbdavw 36494. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑦⦌𝐷)
Theorem	cbvrabdavw 36496*	Change bound variable in restricted class abstractions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∈ 𝐴 ∣ 𝜒})
Theorem	cbviundavw 36497*	Change bound variable in indexed unions. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbviindavw 36498*	Change bound variable in indexed intersections. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶)
Theorem	cbvopab1davw 36499*	Change the first bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑧, 𝑦⟩ ∣ 𝜒})
Theorem	cbvopab2davw 36500*	Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025.)
⊢ ((𝜑 ∧ 𝑦 = 𝑧) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑧⟩ ∣ 𝜒})