Metamath Proof Explorer


Theorem cbv2

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbv2w with disjoint variable conditions, not depending on ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style, avoid ax-10 . (Revised by Wolf Lammen, 10-Sep-2023) (New usage is discouraged.)

Ref Expression
Hypotheses cbv2.1 𝑥 𝜑
cbv2.2 𝑦 𝜑
cbv2.3 ( 𝜑 → Ⅎ 𝑦 𝜓 )
cbv2.4 ( 𝜑 → Ⅎ 𝑥 𝜒 )
cbv2.5 ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
Assertion cbv2 ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )

Proof

Step Hyp Ref Expression
1 cbv2.1 𝑥 𝜑
2 cbv2.2 𝑦 𝜑
3 cbv2.3 ( 𝜑 → Ⅎ 𝑦 𝜓 )
4 cbv2.4 ( 𝜑 → Ⅎ 𝑥 𝜒 )
5 cbv2.5 ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
6 biimp ( ( 𝜓𝜒 ) → ( 𝜓𝜒 ) )
7 5 6 syl6 ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓𝜒 ) ) )
8 1 2 3 4 7 cbv1 ( 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑦 𝜒 ) )
9 equcomi ( 𝑦 = 𝑥𝑥 = 𝑦 )
10 biimpr ( ( 𝜓𝜒 ) → ( 𝜒𝜓 ) )
11 9 5 10 syl56 ( 𝜑 → ( 𝑦 = 𝑥 → ( 𝜒𝜓 ) ) )
12 2 1 4 3 11 cbv1 ( 𝜑 → ( ∀ 𝑦 𝜒 → ∀ 𝑥 𝜓 ) )
13 8 12 impbid ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑦 𝜒 ) )