Description: Under a non-freeness hypothesis, the implication 19.38 can be strengthened to an equivalence. See also 19.38a . (Contributed by BJ, 3-Nov-2021) (Proof shortened by Wolf Lammen, 9-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | 19.38b |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.38 | ||
2 | exim | ||
3 | id | ||
4 | 3 | nfrd | |
5 | 2 4 | syl9r | |
6 | 1 5 | impbid2 |