Metamath Proof Explorer

Theorem axacprim

Description: ax-ac without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010)

Ref Expression
Assertion axacprim ⊢¬∀x¬∀y∀z∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x

Proof

Step Hyp Ref Expression
1 axacnd ⊢∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
2 df-an ⊢y∈z∧z∈w↔¬y∈z→¬z∈w
3 2 albii ⊢∀xy∈z∧z∈w↔∀x¬y∈z→¬z∈w
4 anass ⊢y∈z∧z∈w∧y∈w∧w∈x↔y∈z∧z∈w∧y∈w∧w∈x
5 annim ⊢z∈w∧¬y∈w→¬w∈x↔¬z∈w→y∈w→¬w∈x
6 pm4.63 ⊢¬y∈w→¬w∈x↔y∈w∧w∈x
7 6 anbi2i ⊢z∈w∧¬y∈w→¬w∈x↔z∈w∧y∈w∧w∈x
8 5 7 bitr3i ⊢¬z∈w→y∈w→¬w∈x↔z∈w∧y∈w∧w∈x
9 8 anbi2i ⊢y∈z∧¬z∈w→y∈w→¬w∈x↔y∈z∧z∈w∧y∈w∧w∈x
10 annim ⊢y∈z∧¬z∈w→y∈w→¬w∈x↔¬y∈z→z∈w→y∈w→¬w∈x
11 4 9 10 3bitr2i ⊢y∈z∧z∈w∧y∈w∧w∈x↔¬y∈z→z∈w→y∈w→¬w∈x
12 11 exbii ⊢∃wy∈z∧z∈w∧y∈w∧w∈x↔∃w¬y∈z→z∈w→y∈w→¬w∈x
13 exnal ⊢∃w¬y∈z→z∈w→y∈w→¬w∈x↔¬∀wy∈z→z∈w→y∈w→¬w∈x
14 12 13 bitri ⊢∃wy∈z∧z∈w∧y∈w∧w∈x↔¬∀wy∈z→z∈w→y∈w→¬w∈x
15 14 bibi1i ⊢∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔¬∀wy∈z→z∈w→y∈w→¬w∈x↔y=w
16 dfbi1 ⊢¬∀wy∈z→z∈w→y∈w→¬w∈x↔y=w↔¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
17 15 16 bitri ⊢∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
18 17 albii ⊢∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
19 18 exbii ⊢∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔∃w∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
20 df-ex ⊢∃w∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x↔¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
21 19 20 bitri ⊢∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
22 3 21 imbi12i ⊢∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
23 22 2albii ⊢∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔∀y∀z∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
24 23 exbii ⊢∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔∃x∀y∀z∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
25 df-ex ⊢∃x∀y∀z∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x↔¬∀x¬∀y∀z∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
26 24 25 bitri ⊢∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w↔¬∀x¬∀y∀z∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x
27 1 26 mpbi ⊢¬∀x¬∀y∀z∀x¬y∈z→¬z∈w→¬∀w¬∀y¬¬∀wy∈z→z∈w→y∈w→¬w∈x→y=w→¬y=w→¬∀wy∈z→z∈w→y∈w→¬w∈x