Theorem ennum

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

	Ref	Expression
Assertion	ennum	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ dom card ↔ 𝐵 ∈ dom card ) )

Proof

Step	Hyp	Ref	Expression
1		enen2	⊢ ( 𝐴 ≈ 𝐵 → ( 𝑥 ≈ 𝐴 ↔ 𝑥 ≈ 𝐵 ) )
2	1	rexbidv	⊢ ( 𝐴 ≈ 𝐵 → ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐵 ) )
3		isnum2	⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 )
4		isnum2	⊢ ( 𝐵 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐵 )
5	2 3 4	3bitr4g	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ dom card ↔ 𝐵 ∈ dom card ) )