Metamath Proof Explorer

Theorem axpowprim

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

Ref Expression
Assertion axpowprim ⊢ ∀ x ¬ ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x → x = y

Proof

Step Hyp Ref Expression
1 axpownd ⊢ ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
2 df-ex ⊢ ∃ z x ∈ y ↔ ¬ ∀ z ¬ x ∈ y
3 2 imbi1i ⊢ ∃ z x ∈ y → ∀ y x ∈ z ↔ ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z
4 3 albii ⊢ ∀ x ∃ z x ∈ y → ∀ y x ∈ z ↔ ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z
5 4 imbi1i ⊢ ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x ↔ ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x
6 5 albii ⊢ ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x ↔ ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x
7 6 exbii ⊢ ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x ↔ ∃ x ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x
8 df-ex ⊢ ∃ x ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x ↔ ¬ ∀ x ¬ ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x
9 7 8 bitri ⊢ ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x ↔ ¬ ∀ x ¬ ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x
10 1 9 sylib ⊢ ¬ x = y → ¬ ∀ x ¬ ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x
11 10 con4i ⊢ ∀ x ¬ ∀ y ∀ x ¬ ∀ z ¬ x ∈ y → ∀ y x ∈ z → y ∈ x → x = y