This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvralf

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvralfw when possible. (Contributed by NM, 7-Mar-2004) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvralf.1 ⊢ Ⅎ 𝑥 𝐴
cbvralf.2 ⊢ Ⅎ 𝑦 𝐴
cbvralf.3 ⊢ Ⅎ 𝑦 𝜑
cbvralf.4 ⊢ Ⅎ 𝑥 𝜓
cbvralf.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion cbvralf ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜓 )

Proof

Step Hyp Ref Expression
1 cbvralf.1 ⊢ Ⅎ 𝑥 𝐴
2 cbvralf.2 ⊢ Ⅎ 𝑦 𝐴
3 cbvralf.3 ⊢ Ⅎ 𝑦 𝜑
4 cbvralf.4 ⊢ Ⅎ 𝑥 𝜓
5 cbvralf.5 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6 nfv ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 → 𝜑 )
7 1 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
8 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
9 7 8 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 )
10 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
11 sbequ12 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
12 10 11 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
13 6 9 12 cbvalv1 ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) )
14 2 nfcri ⊢ Ⅎ 𝑦 𝑧 ∈ 𝐴
15 3 nfsb ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
16 14 15 nfim ⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 )
17 nfv ⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐴 → 𝜓 )
18 eleq1w ⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
19 sbequ ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
20 4 5 sbie ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
21 19 20 bitrdi ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
22 18 21 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → 𝜓 ) ) )
23 16 17 22 cbvalv1 ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
24 13 23 bitri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
25 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
26 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 𝜓 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
27 24 25 26 3bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜓 )