Theorem hfext

Description: Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	hfext	Could not format assertion : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A = B <-> A. x e. HF ( x e. A <-> x e. B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$
2		unvdif	Could not format ( HF u. ( _V \ HF ) ) = _V : No typesetting found for |- ( HF u. ( _V \ HF ) ) = _V with typecode |-
3	2	raleqi	Could not format ( A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) <-> A. x e. _V ( x e. A <-> x e. B ) ) : No typesetting found for |- ( A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) <-> A. x e. _V ( x e. A <-> x e. B ) ) with typecode |-
4		ralv	$$⊢\forall x\in \mathrm{V}\left(x\in A\leftrightarrow x\in B\right)\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$
5	3 4	bitr2i	Could not format ( A. x ( x e. A <-> x e. B ) <-> A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) ) : No typesetting found for |- ( A. x ( x e. A <-> x e. B ) <-> A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) ) with typecode |-
6		ralunb	Could not format ( A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) <-> ( A. x e. HF ( x e. A <-> x e. B ) /\ A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) ) : No typesetting found for |- ( A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) <-> ( A. x e. HF ( x e. A <-> x e. B ) /\ A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) ) with typecode |-
7	1 5 6	3bitri	Could not format ( A = B <-> ( A. x e. HF ( x e. A <-> x e. B ) /\ A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) ) : No typesetting found for |- ( A = B <-> ( A. x e. HF ( x e. A <-> x e. B ) /\ A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) ) with typecode |-
8		vex	$$⊢x\in \mathrm{V}$$
9		eldif	Could not format ( x e. ( _V \ HF ) <-> ( x e. _V /\ -. x e. HF ) ) : No typesetting found for |- ( x e. ( _V \ HF ) <-> ( x e. _V /\ -. x e. HF ) ) with typecode |-
10	8 9	mpbiran	Could not format ( x e. ( _V \ HF ) <-> -. x e. HF ) : No typesetting found for |- ( x e. ( _V \ HF ) <-> -. x e. HF ) with typecode |-
11		hfelhf	Could not format ( ( x e. A /\ A e. HF ) -> x e. HF ) : No typesetting found for |- ( ( x e. A /\ A e. HF ) -> x e. HF ) with typecode |-
12	11	stoic1b	Could not format ( ( A e. HF /\ -. x e. HF ) -> -. x e. A ) : No typesetting found for |- ( ( A e. HF /\ -. x e. HF ) -> -. x e. A ) with typecode |-
13	12	adantlr	Could not format ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> -. x e. A ) : No typesetting found for |- ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> -. x e. A ) with typecode |-
14		hfelhf	Could not format ( ( x e. B /\ B e. HF ) -> x e. HF ) : No typesetting found for |- ( ( x e. B /\ B e. HF ) -> x e. HF ) with typecode |-
15	14	stoic1b	Could not format ( ( B e. HF /\ -. x e. HF ) -> -. x e. B ) : No typesetting found for |- ( ( B e. HF /\ -. x e. HF ) -> -. x e. B ) with typecode |-
16	15	adantll	Could not format ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> -. x e. B ) : No typesetting found for |- ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> -. x e. B ) with typecode |-
17	13 16	2falsed	Could not format ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> ( x e. A <-> x e. B ) ) : No typesetting found for |- ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> ( x e. A <-> x e. B ) ) with typecode |-
18	10 17	sylan2b	Could not format ( ( ( A e. HF /\ B e. HF ) /\ x e. ( _V \ HF ) ) -> ( x e. A <-> x e. B ) ) : No typesetting found for |- ( ( ( A e. HF /\ B e. HF ) /\ x e. ( _V \ HF ) ) -> ( x e. A <-> x e. B ) ) with typecode |-
19	18	ralrimiva	Could not format ( ( A e. HF /\ B e. HF ) -> A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) with typecode |-
20	19	biantrud	Could not format ( ( A e. HF /\ B e. HF ) -> ( A. x e. HF ( x e. A <-> x e. B ) <-> ( A. x e. HF ( x e. A <-> x e. B ) /\ A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) ) ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A. x e. HF ( x e. A <-> x e. B ) <-> ( A. x e. HF ( x e. A <-> x e. B ) /\ A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) ) ) with typecode |-
21	7 20	bitr4id	Could not format ( ( A e. HF /\ B e. HF ) -> ( A = B <-> A. x e. HF ( x e. A <-> x e. B ) ) ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A = B <-> A. x e. HF ( x e. A <-> x e. B ) ) ) with typecode |-