Description: Alternate elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ceqsralv2.1 | ||
Assertion | ceqsralv2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsralv2.1 | ||
2 | 1 | notbid | |
3 | 2 | ceqsrexv2 | |
4 | rexanali | ||
5 | annim | ||
6 | 3 4 5 | 3bitr3i | |
7 | 6 | con4bii |