Theorem sb8iota

Description: Variable substitution in description binder. Compare sb8eu . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 18-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sb8iota.1	⊢ Ⅎ 𝑦 𝜑
Assertion	sb8iota	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sb8iota.1	⊢ Ⅎ 𝑦 𝜑
2		nfv	⊢ Ⅎ 𝑤 ( 𝜑 ↔ 𝑥 = 𝑧 )
3	2	sb8	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑤 [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) )
4		sbbi	⊢ ( [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝑥 = 𝑧 ) )
5	1	nfsb	⊢ Ⅎ 𝑦 [ 𝑤 / 𝑥 ] 𝜑
6		equsb3	⊢ ( [ 𝑤 / 𝑥 ] 𝑥 = 𝑧 ↔ 𝑤 = 𝑧 )
7		nfv	⊢ Ⅎ 𝑦 𝑤 = 𝑧
8	6 7	nfxfr	⊢ Ⅎ 𝑦 [ 𝑤 / 𝑥 ] 𝑥 = 𝑧
9	5 8	nfbi	⊢ Ⅎ 𝑦 ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝑥 = 𝑧 )
10	4 9	nfxfr	⊢ Ⅎ 𝑦 [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 )
11		nfv	⊢ Ⅎ 𝑤 [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 )
12		sbequ	⊢ ( 𝑤 = 𝑦 → ( [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ) )
13	10 11 12	cbvalv1	⊢ ( ∀ 𝑤 [ 𝑤 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) )
14		equsb3	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 )
15	14	sblbis	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) )
16	15	albii	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) )
17	3 13 16	3bitri	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) )
18	17	abbii	⊢ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = { 𝑧 ∣ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) }
19	18	unieqi	⊢ ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = ∪ { 𝑧 ∣ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) }
20		dfiota2	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) }
21		dfiota2	⊢ ( ℩ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) = ∪ { 𝑧 ∣ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = 𝑧 ) }
22	19 20 21	3eqtr4i	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )