Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finite sets
enfi
Next ⟩
enfii
Metamath Proof Explorer
Ascii
Unicode
Theorem
enfi
Description:
Equinumerous sets have the same finiteness.
(Contributed by
NM
, 22-Aug-2008)
Ref
Expression
Assertion
enfi
⊢
A
≈
B
→
A
∈
Fin
↔
B
∈
Fin
Proof
Step
Hyp
Ref
Expression
1
enen1
⊢
A
≈
B
→
A
≈
x
↔
B
≈
x
2
1
rexbidv
⊢
A
≈
B
→
∃
x
∈
ω
A
≈
x
↔
∃
x
∈
ω
B
≈
x
3
isfi
⊢
A
∈
Fin
↔
∃
x
∈
ω
A
≈
x
4
isfi
⊢
B
∈
Fin
↔
∃
x
∈
ω
B
≈
x
5
2
3
4
3bitr4g
⊢
A
≈
B
→
A
∈
Fin
↔
B
∈
Fin