Theorem reubidv 3381

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 3379	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564  df-eu 2594  df-reu 3366

This theorem is used by:  reueqd  3399  sbcreu  3822  oawordeu  8566  xpf1o  9161  dfac2b  10212  creur  12317  creui  12318  divalg  16578  divalg2  16580  lubfval  18527  lubeldm  18530  lubval  18533  glbfval  18540  glbeldm  18543  glbval  18546  joineu  18559  meeteu  18573  dfod2  19783  ustuqtop  24570  addsq2reu  27772  addsqn2reu  27773  addsqrexnreu  27774  addsqnreup  27775  2sqreulem1  27778  2sqreunnlem1  27781  angmgmaddov1  29393  angmgmaddov2  29394  usgredg2vtxeuALT  29808  isfrgr  30866  frcond1  30872  frgr1v  30877  nfrgr2v  30878  frgr3v  30881  3vfriswmgr  30884  n4cyclfrgr  30897  eulplig  31092  riesz4  32671  cnlnadjeu  32685  poimirlem25  38656  poimirlem26  38657  hdmap1eulem  42972  hdmap1eulemOLDN  42973  hdmap14lem6  43023  reuf1odnf  48270  euoreqb  48272  isuspgrim0  49085  isuspgrimlem  49086  joindm3  50176  meetdm3  50178  upciclem1  50375  upfval2  50386  upfval3  50387  isuplem  50388  oppcup3lem  50415  isinito2lem  50726