Theorem elkarden

Description: Any member of the kard cardinal number of a set is equinumerous to the set. Contrast with cardne for card cardinals. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	elkarden	⊢ ( 𝐴 ∈ ( kard ‘ 𝐵 ) → 𝐴 ≈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≈ 𝐵 ↔ 𝐴 ≈ 𝐵 ) )
2		fveq2	⊢ ( 𝑥 = 𝐴 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
3	2	sseq1d	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑦 ) ) )
4	3	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
5	4	albidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
6	1 5	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝐴 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
7		kardval2	⊢ ( kard ‘ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
8	6 7	elab2g	⊢ ( 𝐴 ∈ ( kard ‘ 𝐵 ) → ( 𝐴 ∈ ( kard ‘ 𝐵 ) ↔ ( 𝐴 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
9	8	ibi	⊢ ( 𝐴 ∈ ( kard ‘ 𝐵 ) → ( 𝐴 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
10	9	simpld	⊢ ( 𝐴 ∈ ( kard ‘ 𝐵 ) → 𝐴 ≈ 𝐵 )