Metamath Proof Explorer

Theorem axac2

Description: Derive ax-ac2 from ax-ac . (Contributed by NM, 19-Dec-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion axac2 ⊢ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v

Proof

Step Hyp Ref Expression
1 dfac2a ⊢ ∀ x ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u → CHOICE
2 ac3 ⊢ ∃ y ∀ z ∈ x z ≠ ∅ → ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u
3 1 2 mpg ⊢ CHOICE
4 dfackm ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
5 3 4 mpbi ⊢ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
6 5 spi ⊢ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v