Theorem cbviota

Description: Change bound variables in a description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbviotaw when possible. (Contributed by Andrew Salmon, 1-Aug-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbviota.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		cbviota.2	⊢ Ⅎ 𝑦 𝜑
3		cbviota.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	nfsb	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
13		nfv	⊢ Ⅎ 𝑦 𝑧 = 𝑤
14	12 13	nfbi	⊢ Ⅎ 𝑦 ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 )
15		nfv	⊢ Ⅎ 𝑧 ( 𝜓 ↔ 𝑦 = 𝑤 )
16		sbequ	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
17	3 1	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
18	16 17	bitrdi	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
19		equequ1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝑤 ↔ 𝑦 = 𝑤 ) )
20	18 19	bibi12d	⊢ ( 𝑧 = 𝑦 → ( ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 ) ↔ ( 𝜓 ↔ 𝑦 = 𝑤 ) ) )
21	14 15 20	cbvalv1	⊢ ( ∀ 𝑧 ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝑧 = 𝑤 ) ↔ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) )
22	11 21	bitri	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) )
23	22	abbii	⊢ { 𝑤 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) } = { 𝑤 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) }
24	23	unieqi	⊢ ∪ { 𝑤 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) } = ∪ { 𝑤 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) }
25		dfiota2	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑤 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) }
26		dfiota2	⊢ ( ℩ 𝑦 𝜓 ) = ∪ { 𝑤 ∣ ∀ 𝑦 ( 𝜓 ↔ 𝑦 = 𝑤 ) }
27	24 25 26	3eqtr4i	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜓 )