Description: Obsolete version of enfii as of 23-Sep-2024. (Contributed by Mario Carneiro, 12-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | enfiiOLD | |- ( ( B e. Fin /\ A ~~ B ) -> A e. Fin ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | enfi | |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) ) |
|
| 2 | 1 | biimparc | |- ( ( B e. Fin /\ A ~~ B ) -> A e. Fin ) |