Metamath Proof Explorer

Theorem axunprim

Description: ax-un without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010)

Ref Expression
Assertion axunprim ⊢ ¬ ∀ x ¬ ∀ y ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x

Proof

Step Hyp Ref Expression
1 axunnd ⊢ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x
2 df-an ⊢ y ∈ x ∧ x ∈ z ↔ ¬ y ∈ x → ¬ x ∈ z
3 2 exbii ⊢ ∃ x y ∈ x ∧ x ∈ z ↔ ∃ x ¬ y ∈ x → ¬ x ∈ z
4 exnal ⊢ ∃ x ¬ y ∈ x → ¬ x ∈ z ↔ ¬ ∀ x y ∈ x → ¬ x ∈ z
5 3 4 bitri ⊢ ∃ x y ∈ x ∧ x ∈ z ↔ ¬ ∀ x y ∈ x → ¬ x ∈ z
6 5 imbi1i ⊢ ∃ x y ∈ x ∧ x ∈ z → y ∈ x ↔ ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x
7 6 albii ⊢ ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x ↔ ∀ y ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x
8 7 exbii ⊢ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x ↔ ∃ x ∀ y ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x
9 df-ex ⊢ ∃ x ∀ y ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x ↔ ¬ ∀ x ¬ ∀ y ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x
10 8 9 bitri ⊢ ∃ x ∀ y ∃ x y ∈ x ∧ x ∈ z → y ∈ x ↔ ¬ ∀ x ¬ ∀ y ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x
11 1 10 mpbi ⊢ ¬ ∀ x ¬ ∀ y ¬ ∀ x y ∈ x → ¬ x ∈ z → y ∈ x