Theorem cbviotaw

Description: Change bound variables in a description binder. Version of cbviota with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 1-Aug-2011) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Hypotheses	cbviotaw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	cbviotaw.2	⊢ Ⅎ 𝑦 𝜑
	cbviotaw.3	⊢ Ⅎ 𝑥 𝜓
Assertion	cbviotaw	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbviotaw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		cbviotaw.2	⊢ Ⅎ 𝑦 𝜑
3		cbviotaw.3	⊢ Ⅎ 𝑥 𝜓
4		nfv	⊢ Ⅎ 𝑧 ( 𝜑 ↔ 𝑥 = 𝑤 )
5		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
6		nfv	⊢ Ⅎ 𝑥 𝑧 = 𝑤
7	5 6	nfbi	⊢ Ⅎ 𝑥 ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 )
8		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
9		equequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑤 ↔ 𝑧 = 𝑤 ) )
10	8 9	bibi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 ) ) )
11	4 7 10	cbvalv1	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∀ 𝑧 ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 ) )
12	2	nfsbv	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
13		nfv	⊢ Ⅎ 𝑦 𝑧 = 𝑤
14	12 13	nfbi	⊢ Ⅎ 𝑦 ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 )
15		nfv	⊢ Ⅎ 𝑧 ( 𝜓 ↔ 𝑦 = 𝑤 )
16	3 1	sbhypf	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
17		equequ1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝑤 ↔ 𝑦 = 𝑤 ) )
18	16 17	bibi12d	⊢ ( 𝑧 = 𝑦 → ( ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 ) ↔ ( 𝜓 ↔ 𝑦 = 𝑤 ) ) )
19	14 15 18	cbvalv1	⊢ ( ∀ 𝑧 ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 ) ↔ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) )
20	11 19	bitri	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) )
21	20	abbii	⊢ { 𝑤 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) } = { 𝑤 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) }
22	21	unieqi	⊢ ∪ { 𝑤 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) } = ∪ { 𝑤 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) }
23		dfiota2	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑤 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) }
24		dfiota2	⊢ ( ℩ 𝑦 𝜓 ) = ∪ { 𝑤 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) }
25	22 23 24	3eqtr4i	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜓 )