Metamath Proof Explorer

Theorem axrepprim

Description: ax-rep without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010)

Ref Expression
Assertion axrepprim ⊢¬∀x¬¬∀y¬∀zφ→z=y→∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x

Proof

Step Hyp Ref Expression
1 axrepnd ⊢∃x∃y∀zφ→z=y→∀z∀yz∈x↔∃x∀zx∈y∧∀yφ
2 df-ex ⊢∃y∀zφ→z=y↔¬∀y¬∀zφ→z=y
3 df-an ⊢∀zx∈y∧∀yφ↔¬∀zx∈y→¬∀yφ
4 3 exbii ⊢∃x∀zx∈y∧∀yφ↔∃x¬∀zx∈y→¬∀yφ
5 exnal ⊢∃x¬∀zx∈y→¬∀yφ↔¬∀x∀zx∈y→¬∀yφ
6 4 5 bitri ⊢∃x∀zx∈y∧∀yφ↔¬∀x∀zx∈y→¬∀yφ
7 6 bibi2i ⊢∀yz∈x↔∃x∀zx∈y∧∀yφ↔∀yz∈x↔¬∀x∀zx∈y→¬∀yφ
8 dfbi1 ⊢∀yz∈x↔¬∀x∀zx∈y→¬∀yφ↔¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x
9 7 8 bitri ⊢∀yz∈x↔∃x∀zx∈y∧∀yφ↔¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x
10 9 albii ⊢∀z∀yz∈x↔∃x∀zx∈y∧∀yφ↔∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x
11 2 10 imbi12i ⊢∃y∀zφ→z=y→∀z∀yz∈x↔∃x∀zx∈y∧∀yφ↔¬∀y¬∀zφ→z=y→∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x
12 11 exbii ⊢∃x∃y∀zφ→z=y→∀z∀yz∈x↔∃x∀zx∈y∧∀yφ↔∃x¬∀y¬∀zφ→z=y→∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x
13 df-ex ⊢∃x¬∀y¬∀zφ→z=y→∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x↔¬∀x¬¬∀y¬∀zφ→z=y→∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x
14 12 13 bitri ⊢∃x∃y∀zφ→z=y→∀z∀yz∈x↔∃x∀zx∈y∧∀yφ↔¬∀x¬¬∀y¬∀zφ→z=y→∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x
15 1 14 mpbi ⊢¬∀x¬¬∀y¬∀zφ→z=y→∀z¬∀yz∈x→¬∀x∀zx∈y→¬∀yφ→¬¬∀x∀zx∈y→¬∀yφ→∀yz∈x