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	⊢ ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ Hf ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
2		unvdif	⊢ ( Hf ∪ ( V ∖ Hf ) ) = V
3	2	raleqi	⊢ ( ∀ 𝑥 ∈ ( Hf ∪ ( V ∖ Hf ) ) ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ V ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
4		ralv	⊢ ( ∀ 𝑥 ∈ V ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
5	3 4	bitr2i	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ ( Hf ∪ ( V ∖ Hf ) ) ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
6		ralunb	⊢ ( ∀ 𝑥 ∈ ( Hf ∪ ( V ∖ Hf ) ) ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∈ Hf ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ ( V ∖ Hf ) ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
7	1 5 6	3bitri	⊢ ( 𝐴 = 𝐵 ↔ ( ∀ 𝑥 ∈ Hf ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ ( V ∖ Hf ) ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
8		vex	⊢ 𝑥 ∈ V
9		eldif	⊢ ( 𝑥 ∈ ( V ∖ Hf ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ Hf ) )
10	8 9	mpbiran	⊢ ( 𝑥 ∈ ( V ∖ Hf ) ↔ ¬ 𝑥 ∈ Hf )
11		hfelhf	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Hf ) → 𝑥 ∈ Hf )
12	11	stoic1b	⊢ ( ( 𝐴 ∈ Hf ∧ ¬ 𝑥 ∈ Hf ) → ¬ 𝑥 ∈ 𝐴 )
13	12	adantlr	⊢ ( ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) ∧ ¬ 𝑥 ∈ Hf ) → ¬ 𝑥 ∈ 𝐴 )
14		hfelhf	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ Hf ) → 𝑥 ∈ Hf )
15	14	stoic1b	⊢ ( ( 𝐵 ∈ Hf ∧ ¬ 𝑥 ∈ Hf ) → ¬ 𝑥 ∈ 𝐵 )
16	15	adantll	⊢ ( ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) ∧ ¬ 𝑥 ∈ Hf ) → ¬ 𝑥 ∈ 𝐵 )
17	13 16	2falsed	⊢ ( ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) ∧ ¬ 𝑥 ∈ Hf ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
18	10 17	sylan2b	⊢ ( ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) ∧ 𝑥 ∈ ( V ∖ Hf ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
19	18	ralrimiva	⊢ ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ∀ 𝑥 ∈ ( V ∖ Hf ) ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
20	19	biantrud	⊢ ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ( ∀ 𝑥 ∈ Hf ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∈ Hf ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ ( V ∖ Hf ) ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) ) )
21	7 20	bitr4id	⊢ ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ Hf ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )