Metamath Proof Explorer

Theorem mh-unprimbi

Description: Shortest possible version of ax-un in primitive symbols. (Contributed by Matthew House, 13-Apr-2026)

Ref Expression
Assertion mh-unprimbi ⊢ ∃ y ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ¬ ∀ y ¬ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ y

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ v = z → v ∈ u ↔ z ∈ u
2 elequ1 ⊢ v = z → v ∈ y ↔ z ∈ y
3 2 imbi2d ⊢ v = z → u ∈ x → v ∈ y ↔ u ∈ x → z ∈ y
4 1 3 imbi12d ⊢ v = z → v ∈ u → u ∈ x → v ∈ y ↔ z ∈ u → u ∈ x → z ∈ y
5 elequ2 ⊢ u = w → v ∈ u ↔ v ∈ w
6 elequ1 ⊢ u = w → u ∈ x ↔ w ∈ x
7 6 imbi1d ⊢ u = w → u ∈ x → v ∈ y ↔ w ∈ x → v ∈ y
8 5 7 imbi12d ⊢ u = w → v ∈ u → u ∈ x → v ∈ y ↔ v ∈ w → w ∈ x → v ∈ y
9 4 8 alcomw ⊢ ∀ v ∀ u v ∈ u → u ∈ x → v ∈ y ↔ ∀ u ∀ v v ∈ u → u ∈ x → v ∈ y
10 impexp ⊢ z ∈ w ∧ w ∈ x → z ∈ y ↔ z ∈ w → w ∈ x → z ∈ y
11 elequ12 ⊢ z = v ∧ w = u → z ∈ w ↔ v ∈ u
12 elequ1 ⊢ w = u → w ∈ x ↔ u ∈ x
13 12 adantl ⊢ z = v ∧ w = u → w ∈ x ↔ u ∈ x
14 elequ1 ⊢ z = v → z ∈ y ↔ v ∈ y
15 14 adantr ⊢ z = v ∧ w = u → z ∈ y ↔ v ∈ y
16 13 15 imbi12d ⊢ z = v ∧ w = u → w ∈ x → z ∈ y ↔ u ∈ x → v ∈ y
17 11 16 imbi12d ⊢ z = v ∧ w = u → z ∈ w → w ∈ x → z ∈ y ↔ v ∈ u → u ∈ x → v ∈ y
18 10 17 bitrid ⊢ z = v ∧ w = u → z ∈ w ∧ w ∈ x → z ∈ y ↔ v ∈ u → u ∈ x → v ∈ y
19 18 cbval2vw ⊢ ∀ z ∀ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ∀ v ∀ u v ∈ u → u ∈ x → v ∈ y
20 bi2.04 ⊢ z ∈ x → w ∈ z → w ∈ y ↔ w ∈ z → z ∈ x → w ∈ y
21 elequ12 ⊢ w = v ∧ z = u → w ∈ z ↔ v ∈ u
22 21 ancoms ⊢ z = u ∧ w = v → w ∈ z ↔ v ∈ u
23 elequ1 ⊢ z = u → z ∈ x ↔ u ∈ x
24 23 adantr ⊢ z = u ∧ w = v → z ∈ x ↔ u ∈ x
25 elequ1 ⊢ w = v → w ∈ y ↔ v ∈ y
26 25 adantl ⊢ z = u ∧ w = v → w ∈ y ↔ v ∈ y
27 24 26 imbi12d ⊢ z = u ∧ w = v → z ∈ x → w ∈ y ↔ u ∈ x → v ∈ y
28 22 27 imbi12d ⊢ z = u ∧ w = v → w ∈ z → z ∈ x → w ∈ y ↔ v ∈ u → u ∈ x → v ∈ y
29 20 28 bitrid ⊢ z = u ∧ w = v → z ∈ x → w ∈ z → w ∈ y ↔ v ∈ u → u ∈ x → v ∈ y
30 29 cbval2vw ⊢ ∀ z ∀ w z ∈ x → w ∈ z → w ∈ y ↔ ∀ u ∀ v v ∈ u → u ∈ x → v ∈ y
31 9 19 30 3bitr4i ⊢ ∀ z ∀ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ∀ z ∀ w z ∈ x → w ∈ z → w ∈ y
32 19.23v ⊢ ∀ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ∃ w z ∈ w ∧ w ∈ x → z ∈ y
33 32 albii ⊢ ∀ z ∀ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y
34 19.21v ⊢ ∀ w z ∈ x → w ∈ z → w ∈ y ↔ z ∈ x → ∀ w w ∈ z → w ∈ y
35 34 albii ⊢ ∀ z ∀ w z ∈ x → w ∈ z → w ∈ y ↔ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ y
36 31 33 35 3bitr3i ⊢ ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ y
37 36 exbii ⊢ ∃ y ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ∃ y ∀ z z ∈ x → ∀ w w ∈ z → w ∈ y
38 df-ex ⊢ ∃ y ∀ z z ∈ x → ∀ w w ∈ z → w ∈ y ↔ ¬ ∀ y ¬ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ y
39 37 38 bitri ⊢ ∃ y ∀ z ∃ w z ∈ w ∧ w ∈ x → z ∈ y ↔ ¬ ∀ y ¬ ∀ z z ∈ x → ∀ w w ∈ z → w ∈ y