Theorem reu4 3367

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)

Hypothesis

Ref	Expression
rmo4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
reu4	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem reu4

Step	Hyp	Ref	Expression
1		reu5 3136	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3366	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
4	3	anbi2i 726	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
5	1, 4	bitri 263	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-cleq 2603  df-clel 2606  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904

This theorem is referenced by:  reuind  3378  oawordeulem  7521  fin23lem23  9031  nqereu  9630  receu  10551  lbreu  10852  cju  10893  fprodser  14518  divalglem9  14962  ndvdssub  14971  qredeu  15210  pj1eu  17932  efgredeu  17988  lspsneu  18944  qtopeu  21329  qtophmeo  21430  minveclem7  23014  ig1peu  23735  coeeu  23785  plydivalg  23858  hlcgreu  25313  mirreu3  25349  trgcopyeu  25498  axcontlem2  25645  usgra2edg1  25912  usgraedgreu  25917  nbgraf1olem1  25970  4cycl2vnunb  26544  frg2wot1  26584  minvecolem7  27123  hlimreui  27480  riesz4i  28306  cdjreui  28675  xreceu  28961  cvmseu  30512  nocvxmin  31090  segconeu  31288  outsideofeu  31408  poimirlem4  32583  bfp  32793  exidu1  32825  rngoideu  32872  lshpsmreu  33414  cdleme  34866  lcfl7N  35808  mapdpg  36013  hdmap14lem6  36183  mpaaeu  36739  icceuelpart  39974  umgr2edg1  40438  umgr2edgneu  40441  usgredgreu  40445  uspgredg2vtxeu  40447  4cycl2vnunb-av  41460  frgr2wwlk1  41494  frgr2wwlkeqm  41496