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∈Hfx∈A↔x∈B

Proof

Step Hyp Ref Expression
1 dfcleq ⊢A=B↔∀xx∈A↔x∈B
2 unvdif ⊢Hf∪V∖Hf=V
3 2 raleqi ⊢∀x∈Hf∪V∖Hfx∈A↔x∈B↔∀x∈Vx∈A↔x∈B
4 ralv ⊢∀x∈Vx∈A↔x∈B↔∀xx∈A↔x∈B
5 3 4 bitr2i ⊢∀xx∈A↔x∈B↔∀x∈Hf∪V∖Hfx∈A↔x∈B
6 ralunb ⊢∀x∈Hf∪V∖Hfx∈A↔x∈B↔∀x∈Hfx∈A↔x∈B∧∀x∈V∖Hfx∈A↔x∈B
7 1 5 6 3bitri ⊢A=B↔∀x∈Hfx∈A↔x∈B∧∀x∈V∖Hfx∈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∖Hfx∈A↔x∈B
20 19 biantrud ⊢A∈Hf∧B∈Hf→∀x∈Hfx∈A↔x∈B↔∀x∈Hfx∈A↔x∈B∧∀x∈V∖Hfx∈A↔x∈B
21 7 20 bitr4id ⊢A∈Hf∧B∈Hf→A=B↔∀x∈Hfx∈A↔x∈B