Theorem eupickb 1056

Description: Existential uniqueness "pick" showing wff equivalence.

Assertion

Ref	Expression
eupickb	⊢ ((∃!xφ ∧ ∃!xψ ∧ ∃x(φ ∧ ψ)) → (φ ↔ ψ))

Proof of Theorem eupickb

Step	Hyp	Ref	Expression
1		eupick 1055	. . 3 ⊢ ((∃!xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
2	1	3adant2 598	. 2 ⊢ ((∃!xφ ∧ ∃!xψ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
3		3simpc 593	. . 3 ⊢ ((∃!xφ ∧ ∃!xψ ∧ ∃x(φ ∧ ψ)) → (∃!xψ ∧ ∃x(φ ∧ ψ)))
4		ancom 333	. . . . . 6 ⊢ ((φ ∧ ψ) ↔ (ψ ∧ φ))
5	4	biimp 133	. . . . 5 ⊢ ((φ ∧ ψ) → (ψ ∧ φ))
6	5	19.22i 723	. . . 4 ⊢ (∃x(φ ∧ ψ) → ∃x(ψ ∧ φ))
7	6	anim2i 270	. . 3 ⊢ ((∃!xψ ∧ ∃x(φ ∧ ψ)) → (∃!xψ ∧ ∃x(ψ ∧ φ)))
8		eupick 1055	. . 3 ⊢ ((∃!xψ ∧ ∃x(ψ ∧ φ)) → (ψ → φ))
9	3, 7, 8	3syl 21	. 2 ⊢ ((∃!xφ ∧ ∃!xψ ∧ ∃x(φ ∧ ψ)) → (ψ → φ))
10	2, 9	impbid 397	1 ⊢ ((∃!xφ ∧ ∃!xψ ∧ ∃x(φ ∧ ψ)) → (φ ↔ ψ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   ∧ w3a 581  ∃wex 678  ∃!weu 1007

This theorem is referenced by:  euuni 1954

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010

metamath.org