Theorem ennum

Description: Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	ennum	$$⊢A\approx B\to \left(A\in \mathrm{dom}\mathrm{card}\leftrightarrow B\in \mathrm{dom}\mathrm{card}\right)$$

Proof

Step	Hyp	Ref	Expression
1		enen2	$$⊢A\approx B\to \left(x\approx A\leftrightarrow x\approx B\right)$$
2	1	rexbidv	$$⊢A\approx B\to \left(\exists x\in \mathrm{On}x\approx A\leftrightarrow \exists x\in \mathrm{On}x\approx B\right)$$
3		isnum2	$$⊢A\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists x\in \mathrm{On}x\approx A$$
4		isnum2	$$⊢B\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists x\in \mathrm{On}x\approx B$$
5	2 3 4	3bitr4g	$$⊢A\approx B\to \left(A\in \mathrm{dom}\mathrm{card}\leftrightarrow B\in \mathrm{dom}\mathrm{card}\right)$$