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 𝑦𝑧𝑣𝑢 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑣𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧𝑣 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑣𝑧𝑣𝑦 ) ∧ ( ( 𝑢𝑧𝑢𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfac2a ( ∀ 𝑥𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) → CHOICE )
2 ac3 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) )
3 1 2 mpg CHOICE
4 dfackm ( CHOICE ↔ ∀ 𝑥𝑦𝑧𝑣𝑢 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑣𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧𝑣 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑣𝑧𝑣𝑦 ) ∧ ( ( 𝑢𝑧𝑢𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )
5 3 4 mpbi 𝑥𝑦𝑧𝑣𝑢 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑣𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧𝑣 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑣𝑧𝑣𝑦 ) ∧ ( ( 𝑢𝑧𝑢𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )
6 5 spi 𝑦𝑧𝑣𝑢 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑣𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧𝑣 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑣𝑧𝑣𝑦 ) ∧ ( ( 𝑢𝑧𝑢𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )