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	|- ( ( A e. HF /\ B e. HF ) -> ( A = B <-> A. x e. HF ( x e. A <-> x e. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2		unvdif	|- ( HF u. ( _V \ HF ) ) = _V
3	2	raleqi	|- ( A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) <-> A. x e. _V ( x e. A <-> x e. B ) )
4		ralv	|- ( A. x e. _V ( x e. A <-> x e. B ) <-> A. x ( x e. A <-> x e. B ) )
5	3 4	bitr2i	|- ( A. x ( x e. A <-> x e. B ) <-> A. x e. ( HF u. ( _V \ HF ) ) ( x e. A <-> x e. B ) )
6		ralunb	|- ( 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 ) ) )
7	1 5 6	3bitri	|- ( A = B <-> ( A. x e. HF ( x e. A <-> x e. B ) /\ A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) ) )
8		vex	|- x e. _V
9		eldif	|- ( x e. ( _V \ HF ) <-> ( x e. _V /\ -. x e. HF ) )
10	8 9	mpbiran	|- ( x e. ( _V \ HF ) <-> -. x e. HF )
11		hfelhf	|- ( ( x e. A /\ A e. HF ) -> x e. HF )
12	11	stoic1b	|- ( ( A e. HF /\ -. x e. HF ) -> -. x e. A )
13	12	adantlr	|- ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> -. x e. A )
14		hfelhf	|- ( ( x e. B /\ B e. HF ) -> x e. HF )
15	14	stoic1b	|- ( ( B e. HF /\ -. x e. HF ) -> -. x e. B )
16	15	adantll	|- ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> -. x e. B )
17	13 16	2falsed	|- ( ( ( A e. HF /\ B e. HF ) /\ -. x e. HF ) -> ( x e. A <-> x e. B ) )
18	10 17	sylan2b	|- ( ( ( A e. HF /\ B e. HF ) /\ x e. ( _V \ HF ) ) -> ( x e. A <-> x e. B ) )
19	18	ralrimiva	|- ( ( A e. HF /\ B e. HF ) -> A. x e. ( _V \ HF ) ( x e. A <-> x e. B ) )
20	19	biantrud	|- ( ( 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 ) ) ) )
21	7 20	bitr4id	|- ( ( A e. HF /\ B e. HF ) -> ( A = B <-> A. x e. HF ( x e. A <-> x e. B ) ) )