Metamath Proof Explorer


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 ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜓 )