Theorem reubidv 3388

Description: Formula-building rule for restricted existential uniqueness quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)

Hypothesis

Ref	Expression
rmobidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
reubidv	⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidv

Step	Hyp	Ref	Expression
1		rmobidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3386	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146  ∃!wreu 3370

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2570  df-eu 2600  df-reu 3373

This theorem is used by:  reueqd  3406  sbcreu  3832  oawordeu  8549  xpf1o  9137  dfac2b  10133  creur  12230  creui  12231  divalg  16486  divalg2  16488  lubfval  18429  lubeldm  18432  lubval  18435  glbfval  18442  glbeldm  18445  glbval  18448  joineu  18461  meeteu  18475  dfod2  19665  ustuqtop  24440  addsq2reu  27641  addsqn2reu  27642  addsqrexnreu  27643  addsqnreup  27644  2sqreulem1  27647  2sqreunnlem1  27650  usgredg2vtxeuALT  29609  isfrgr  30648  frcond1  30654  frgr1v  30659  nfrgr2v  30660  frgr3v  30663  3vfriswmgr  30666  n4cyclfrgr  30679  eulplig  30874  riesz4  32453  cnlnadjeu  32467  poimirlem25  38337  poimirlem26  38338  hdmap1eulem  42637  hdmap1eulemOLDN  42638  hdmap14lem6  42688  reuf1odnf  47885  euoreqb  47887  isuspgrim0  48700  isuspgrimlem  48701  joindm3  49788  meetdm3  49790  upciclem1  49985  upfval2  49996  upfval3  49997  isuplem  49998  oppcup3lem  50025  isinito2lem  50317