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	Could not format assertion : No typesetting found for |- ( A e. ( kard ` B ) -> A ~~ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢x=A\to \left(x\approx B\leftrightarrow A\approx B\right)$$
2		fveq2	$$⊢x=A\to \mathrm{rank}\left(x\right)=\mathrm{rank}\left(A\right)$$
3	2	sseq1d	$$⊢x=A\to \left(\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\leftrightarrow \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
4	3	imbi2d	$$⊢x=A\to \left(\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \left(y\approx B\to \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
5	4	albidv	$$⊢x=A\to \left(\forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\leftrightarrow \forall y\left(y\approx B\to \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)$$
6	1 5	anbi12d	$$⊢x=A\to \left(\left(x\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\leftrightarrow \left(A\approx B\wedge \forall y\left(y\approx B\to \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(y\right)\right)\right)\right)$$
7		kardval2	Could not format ( kard ` B ) = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) } : No typesetting found for |- ( kard ` B ) = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) } with typecode |-
8	6 7	elab2g	Could not format ( A e. ( kard ` B ) -> ( A e. ( kard ` B ) <-> ( A ~~ B /\ A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) ) ) : No typesetting found for |- ( A e. ( kard ` B ) -> ( A e. ( kard ` B ) <-> ( A ~~ B /\ A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) ) ) with typecode |-
9	8	ibi	Could not format ( A e. ( kard ` B ) -> ( A ~~ B /\ A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) ) : No typesetting found for |- ( A e. ( kard ` B ) -> ( A ~~ B /\ A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) ) with typecode |-
10	9	simpld	Could not format ( A e. ( kard ` B ) -> A ~~ B ) : No typesetting found for |- ( A e. ( kard ` B ) -> A ~~ B ) with typecode |-