Theorem hftr

Description: The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	hftr	Could not format assertion : No typesetting found for |- Tr HF with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dftr2	Could not format ( Tr HF <-> A. x A. y ( ( x e. y /\ y e. HF ) -> x e. HF ) ) : No typesetting found for |- ( Tr HF <-> A. x A. y ( ( x e. y /\ y e. HF ) -> x e. HF ) ) with typecode |-
2		hfelhf	Could not format ( ( x e. y /\ y e. HF ) -> x e. HF ) : No typesetting found for |- ( ( x e. y /\ y e. HF ) -> x e. HF ) with typecode |-
3	2	ax-gen	Could not format A. y ( ( x e. y /\ y e. HF ) -> x e. HF ) : No typesetting found for |- A. y ( ( x e. y /\ y e. HF ) -> x e. HF ) with typecode |-
4	1 3	mpgbir	Could not format Tr HF : No typesetting found for |- Tr HF with typecode |-