Metamath Proof Explorer


Theorem cbval2vOLD

Description: Obsolete version of cbval2v as of 14-Jan-2024. (Contributed by BJ, 16-Jan-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cbval2v.1 𝑧 𝜑
cbval2v.2 𝑤 𝜑
cbval2v.3 𝑥 𝜓
cbval2v.4 𝑦 𝜓
cbval2v.5 ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → ( 𝜑𝜓 ) )
Assertion cbval2vOLD ( ∀ 𝑥𝑦 𝜑 ↔ ∀ 𝑧𝑤 𝜓 )

Proof

Step Hyp Ref Expression
1 cbval2v.1 𝑧 𝜑
2 cbval2v.2 𝑤 𝜑
3 cbval2v.3 𝑥 𝜓
4 cbval2v.4 𝑦 𝜓
5 cbval2v.5 ( ( 𝑥 = 𝑧𝑦 = 𝑤 ) → ( 𝜑𝜓 ) )
6 1 nfal 𝑧𝑦 𝜑
7 3 nfal 𝑥𝑤 𝜓
8 nfv 𝑤 𝑥 = 𝑧
9 8 2 nfim 𝑤 ( 𝑥 = 𝑧𝜑 )
10 nfv 𝑦 𝑥 = 𝑧
11 10 4 nfim 𝑦 ( 𝑥 = 𝑧𝜓 )
12 5 expcom ( 𝑦 = 𝑤 → ( 𝑥 = 𝑧 → ( 𝜑𝜓 ) ) )
13 12 pm5.74d ( 𝑦 = 𝑤 → ( ( 𝑥 = 𝑧𝜑 ) ↔ ( 𝑥 = 𝑧𝜓 ) ) )
14 9 11 13 cbvalv1 ( ∀ 𝑦 ( 𝑥 = 𝑧𝜑 ) ↔ ∀ 𝑤 ( 𝑥 = 𝑧𝜓 ) )
15 19.21v ( ∀ 𝑦 ( 𝑥 = 𝑧𝜑 ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) )
16 19.21v ( ∀ 𝑤 ( 𝑥 = 𝑧𝜓 ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑤 𝜓 ) )
17 14 15 16 3bitr3i ( ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑤 𝜓 ) )
18 17 pm5.74ri ( 𝑥 = 𝑧 → ( ∀ 𝑦 𝜑 ↔ ∀ 𝑤 𝜓 ) )
19 6 7 18 cbvalv1 ( ∀ 𝑥𝑦 𝜑 ↔ ∀ 𝑧𝑤 𝜓 )