Metamath Proof Explorer

Theorem 2reuimp

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification if the class of the quantified elements is not empty. (Contributed by AV, 13-Mar-2023)

Ref Expression
Hypotheses 2reuimp.c ⊢ b = c → φ ↔ θ
2reuimp.d ⊢ a = d → φ ↔ χ
2reuimp.a ⊢ a = d → θ ↔ τ
2reuimp.e ⊢ b = e → φ ↔ η
2reuimp.f ⊢ c = f → θ ↔ ψ
Assertion 2reuimp ⊢ V ≠ ∅ ∧ ∃! a ∈ V ∃! b ∈ V φ → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f

Proof

Step Hyp Ref Expression
1 2reuimp.c ⊢ b = c → φ ↔ θ
2 2reuimp.d ⊢ a = d → φ ↔ χ
3 2reuimp.a ⊢ a = d → θ ↔ τ
4 2reuimp.e ⊢ b = e → φ ↔ η
5 2reuimp.f ⊢ c = f → θ ↔ ψ
6 r19.28zv ⊢ V ≠ ∅ → ∀ c ∈ V χ ∧ τ → b = c ↔ χ ∧ ∀ c ∈ V τ → b = c
7 6 bicomd ⊢ V ≠ ∅ → χ ∧ ∀ c ∈ V τ → b = c ↔ ∀ c ∈ V χ ∧ τ → b = c
8 7 imbi1d ⊢ V ≠ ∅ → χ ∧ ∀ c ∈ V τ → b = c → a = d ↔ ∀ c ∈ V χ ∧ τ → b = c → a = d
9 r19.36zv ⊢ V ≠ ∅ → ∃ c ∈ V χ ∧ τ → b = c → a = d ↔ ∀ c ∈ V χ ∧ τ → b = c → a = d
10 r19.42v ⊢ ∃ c ∈ V η ∧ ψ → e = f ∧ χ ∧ τ → b = c → a = d ↔ η ∧ ψ → e = f ∧ ∃ c ∈ V χ ∧ τ → b = c → a = d
11 pm5.31r ⊢ η ∧ ψ → e = f → ψ → η ∧ e = f
12 pm5.31r ⊢ ψ → η ∧ e = f ∧ χ ∧ τ → b = c → a = d → χ ∧ τ → b = c → ψ → η ∧ e = f ∧ a = d
13 pm5.31r ⊢ a = d ∧ ψ → η ∧ e = f → ψ → a = d ∧ η ∧ e = f
14 an12 ⊢ a = d ∧ η ∧ e = f ↔ η ∧ a = d ∧ e = f
15 13 14 syl6ib ⊢ a = d ∧ ψ → η ∧ e = f → ψ → η ∧ a = d ∧ e = f
16 15 ancoms ⊢ ψ → η ∧ e = f ∧ a = d → ψ → η ∧ a = d ∧ e = f
17 12 16 syl6 ⊢ ψ → η ∧ e = f ∧ χ ∧ τ → b = c → a = d → χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
18 11 17 sylan ⊢ η ∧ ψ → e = f ∧ χ ∧ τ → b = c → a = d → χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
19 18 reximi ⊢ ∃ c ∈ V η ∧ ψ → e = f ∧ χ ∧ τ → b = c → a = d → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
20 10 19 sylbir ⊢ η ∧ ψ → e = f ∧ ∃ c ∈ V χ ∧ τ → b = c → a = d → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
21 20 expcom ⊢ ∃ c ∈ V χ ∧ τ → b = c → a = d → η ∧ ψ → e = f → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
22 21 expd ⊢ ∃ c ∈ V χ ∧ τ → b = c → a = d → η → ψ → e = f → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
23 9 22 syl6bir ⊢ V ≠ ∅ → ∀ c ∈ V χ ∧ τ → b = c → a = d → η → ψ → e = f → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
24 8 23 sylbid ⊢ V ≠ ∅ → χ ∧ ∀ c ∈ V τ → b = c → a = d → η → ψ → e = f → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
25 24 com23 ⊢ V ≠ ∅ → η → χ ∧ ∀ c ∈ V τ → b = c → a = d → ψ → e = f → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
26 25 imp4c ⊢ V ≠ ∅ → η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f → ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
27 26 ralimdv ⊢ V ≠ ∅ → ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f → ∀ f ∈ V ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
28 27 reximdv ⊢ V ≠ ∅ → ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f → ∃ e ∈ V ∀ f ∈ V ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
29 28 ralimdv ⊢ V ≠ ∅ → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f → ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
30 29 ralimdv ⊢ V ≠ ∅ → ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f → ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
31 30 reximdv ⊢ V ≠ ∅ → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f
32 1 2 3 4 5 2reuimp0 ⊢ ∃! a ∈ V ∃! b ∈ V φ → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V η ∧ χ ∧ ∀ c ∈ V τ → b = c → a = d ∧ ψ → e = f
33 31 32 impel ⊢ V ≠ ∅ ∧ ∃! a ∈ V ∃! b ∈ V φ → ∃ a ∈ V ∀ d ∈ V ∀ b ∈ V ∃ e ∈ V ∀ f ∈ V ∃ c ∈ V χ ∧ τ → b = c → ψ → η ∧ a = d ∧ e = f