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