Metamath Proof Explorer

Theorem aceq0

Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac . (Contributed by NM, 5-Apr-2004)

Ref Expression
Assertion aceq0 ⊢∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∃y∀z∀wz∈w∧w∈x→∃v∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v

Proof

Step Hyp Ref Expression
1 aceq1 ⊢∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
2 equequ2 ⊢v=x→u=v↔u=x
3 2 bibi2d ⊢v=x→∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔∃tu∈w∧w∈t∧u∈t∧t∈y↔u=x
4 elequ2 ⊢t=x→w∈t↔w∈x
5 4 anbi2d ⊢t=x→u∈w∧w∈t↔u∈w∧w∈x
6 elequ2 ⊢t=x→u∈t↔u∈x
7 elequ1 ⊢t=x→t∈y↔x∈y
8 6 7 anbi12d ⊢t=x→u∈t∧t∈y↔u∈x∧x∈y
9 5 8 anbi12d ⊢t=x→u∈w∧w∈t∧u∈t∧t∈y↔u∈w∧w∈x∧u∈x∧x∈y
10 9 cbvexvw ⊢∃tu∈w∧w∈t∧u∈t∧t∈y↔∃xu∈w∧w∈x∧u∈x∧x∈y
11 10 bibi1i ⊢∃tu∈w∧w∈t∧u∈t∧t∈y↔u=x↔∃xu∈w∧w∈x∧u∈x∧x∈y↔u=x
12 3 11 bitrdi ⊢v=x→∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔∃xu∈w∧w∈x∧u∈x∧x∈y↔u=x
13 12 albidv ⊢v=x→∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔∀u∃xu∈w∧w∈x∧u∈x∧x∈y↔u=x
14 elequ1 ⊢u=z→u∈w↔z∈w
15 14 anbi1d ⊢u=z→u∈w∧w∈x↔z∈w∧w∈x
16 elequ1 ⊢u=z→u∈x↔z∈x
17 16 anbi1d ⊢u=z→u∈x∧x∈y↔z∈x∧x∈y
18 15 17 anbi12d ⊢u=z→u∈w∧w∈x∧u∈x∧x∈y↔z∈w∧w∈x∧z∈x∧x∈y
19 18 exbidv ⊢u=z→∃xu∈w∧w∈x∧u∈x∧x∈y↔∃xz∈w∧w∈x∧z∈x∧x∈y
20 equequ1 ⊢u=z→u=x↔z=x
21 19 20 bibi12d ⊢u=z→∃xu∈w∧w∈x∧u∈x∧x∈y↔u=x↔∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
22 21 cbvalvw ⊢∀u∃xu∈w∧w∈x∧u∈x∧x∈y↔u=x↔∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
23 13 22 bitrdi ⊢v=x→∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
24 23 cbvexvw ⊢∃v∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
25 24 imbi2i ⊢z∈w∧w∈x→∃v∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔z∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
26 25 2albii ⊢∀z∀wz∈w∧w∈x→∃v∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
27 26 exbii ⊢∃y∀z∀wz∈w∧w∈x→∃v∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v↔∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
28 1 27 bitr4i ⊢∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∃y∀z∀wz∈w∧w∈x→∃v∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v