Metamath Proof Explorer

Theorem axac

Description: Derive ax-ac from ax-ac2 . Note that ax-reg is used by the proof. (Contributed by NM, 19-Dec-2016) (Proof modification is discouraged.)

Ref Expression
Assertion axac ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v

Proof

Step Hyp Ref Expression
1 axac3 ⊢ CHOICE
2 dfac0 ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
3 1 2 mpbi ⊢ ∀ x ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
4 3 spi ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v