Description: A reformulation of the axiom of regularity using elementwise intersection. (RK: might have to be placed later since theorems in this section are to be moved early (in the section related to the algebra of sets).) (Contributed by BJ, 27-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-restreg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ∅ ∈ ( 𝐴 ↾t 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zfreg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) | |
| 2 | eqcom | ⊢ ( ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ∅ = ( 𝑥 ∩ 𝐴 ) ) | |
| 3 | 2 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∅ = ( 𝑥 ∩ 𝐴 ) ) |
| 4 | 1 3 | sylib | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∅ = ( 𝑥 ∩ 𝐴 ) ) |
| 5 | simpl | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ 𝑉 ) | |
| 6 | elrest | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ∅ ∈ ( 𝐴 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ∅ = ( 𝑥 ∩ 𝐴 ) ) ) | |
| 7 | 5 6 | syldan | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ∅ ∈ ( 𝐴 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ∅ = ( 𝑥 ∩ 𝐴 ) ) ) |
| 8 | 4 7 | mpbird | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ∅ ∈ ( 𝐴 ↾t 𝐴 ) ) |