Metamath Proof Explorer


Theorem spcdvw

Description: A version of spcdv where ps and ch are direct substitutions of each other. This theorem is useful because it does not require ph and x to be distinct variables. (Contributed by Emmett Weisz, 12-Apr-2020)

Ref Expression
Hypotheses spcdvw.1 ( 𝜑𝐴𝐵 )
spcdvw.2 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) )
Assertion spcdvw ( 𝜑 → ( ∀ 𝑥 𝜓𝜒 ) )

Proof

Step Hyp Ref Expression
1 spcdvw.1 ( 𝜑𝐴𝐵 )
2 spcdvw.2 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) )
3 2 biimpd ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) )
4 3 ax-gen 𝑥 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) )
5 nfv 𝑥 𝜒
6 nfcv 𝑥 𝐴
7 5 6 spcimgft ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜓𝜒 ) ) → ( 𝐴𝐵 → ( ∀ 𝑥 𝜓𝜒 ) ) )
8 4 1 7 mpsyl ( 𝜑 → ( ∀ 𝑥 𝜓𝜒 ) )