Description: Obsolete version of enfi as of 23-Sep-2024. (Contributed by NM, 22-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | enfiOLD | |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | enen1 | |- ( A ~~ B -> ( A ~~ x <-> B ~~ x ) ) |
|
| 2 | 1 | rexbidv | |- ( A ~~ B -> ( E. x e. _om A ~~ x <-> E. x e. _om B ~~ x ) ) |
| 3 | isfi | |- ( A e. Fin <-> E. x e. _om A ~~ x ) |
|
| 4 | isfi | |- ( B e. Fin <-> E. x e. _om B ~~ x ) |
|
| 5 | 2 3 4 | 3bitr4g | |- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) ) |