Theorem reurex 3381

Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)

Assertion

Ref	Expression
reurex	⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Proof of Theorem reurex

Step	Hyp	Ref	Expression
1		reu5 3379	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2	1	simplbi 499	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3071  ∃!wreu 3375  ∃*wrmo 3376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398  df-eu 2564  df-rex 3072  df-rmo 3377  df-reu 3378

This theorem is referenced by:  2reu2rex  3391  reu3  3724  reuxfr1d  3747  2rexreu  3759  sbcreu  3871  reu0  4359  2reu4  4527  tz6.26OLD  6350  weniso  7351  oawordex  8557  oaabs  8647  oaabs2  8648  supval2  9450  fisup2g  9463  fiinf2g  9495  nqerf  10925  qbtwnre  13178  modprm0  16738  issrgid  20027  isringid  20088  lspsneu  20736  frgpcyg  21129  qtophmeo  23321  pjthlem2  24955  dyadmax  25115  quotlem  25813  2sqreulem1  26949  2sqreunnlem1  26952  nfrgr2v  29556  2pthfrgrrn  29566  frgrncvvdeqlem9  29591  frgr2wwlkn0  29612  pjhthlem2  30676  cnlnadj  31363  2reu2rex1  31752  rmoxfrd  31764  cvmliftpht  34340  finorwe  36311  lcfl7N  40420  renegeulem  41290  resubeqsub  41350  requad1  46338  requad2  46339  isringrng  46705  uzlidlring  46875  lubeldm2  47637  glbeldm2  47638