Description: The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | zfregfr | ⊢ E Fr 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfepfr | ⊢ ( E Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) ) | |
2 | vex | ⊢ 𝑥 ∈ V | |
3 | zfreg | ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∩ 𝑥 ) = ∅ ) | |
4 | 2 3 | mpan | ⊢ ( 𝑥 ≠ ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∩ 𝑥 ) = ∅ ) |
5 | incom | ⊢ ( 𝑦 ∩ 𝑥 ) = ( 𝑥 ∩ 𝑦 ) | |
6 | 5 | eqeq1i | ⊢ ( ( 𝑦 ∩ 𝑥 ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) = ∅ ) |
7 | 6 | rexbii | ⊢ ( ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∩ 𝑥 ) = ∅ ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) |
8 | 4 7 | sylib | ⊢ ( 𝑥 ≠ ∅ → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) |
9 | 8 | adantl | ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ( 𝑥 ∩ 𝑦 ) = ∅ ) |
10 | 1 9 | mpgbir | ⊢ E Fr 𝐴 |