Metamath Proof Explorer

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 ∈ Hf ∧ B ∈ Hf → A = B ↔ ∀ x ∈ Hf x ∈ A ↔ x ∈ B

Proof

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