Metamath Proof Explorer


Theorem ceqsralv2

Description: Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020)

Ref Expression
Hypothesis ceqsralv2.1 x = A φ ψ
Assertion ceqsralv2 x B x = A φ A B ψ

Proof

Step Hyp Ref Expression
1 ceqsralv2.1 x = A φ ψ
2 1 notbid x = A ¬ φ ¬ ψ
3 2 ceqsrexv2 x B x = A ¬ φ A B ¬ ψ
4 rexanali x B x = A ¬ φ ¬ x B x = A φ
5 annim A B ¬ ψ ¬ A B ψ
6 3 4 5 3bitr3i ¬ x B x = A φ ¬ A B ψ
7 6 con4bii x B x = A φ A B ψ