Theorem reubidv 3374

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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3372	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∃!wreu 3354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2534  df-eu 2563  df-reu 3357

This theorem is referenced by:  reueqd  3395  sbcreu  3842  oawordeu  8522  xpf1o  9109  dfac2b  10091  creur  12187  creui  12188  divalg  16380  divalg2  16382  lubfval  18316  lubeldm  18319  lubval  18322  glbfval  18329  glbeldm  18332  glbval  18335  joineu  18348  meeteu  18362  dfod2  19501  ustuqtop  24141  addsq2reu  27358  addsqn2reu  27359  addsqrexnreu  27360  addsqnreup  27361  2sqreulem1  27364  2sqreunnlem1  27367  usgredg2vtxeuALT  29156  isfrgr  30196  frcond1  30202  frgr1v  30207  nfrgr2v  30208  frgr3v  30211  3vfriswmgr  30214  n4cyclfrgr  30227  eulplig  30421  riesz4  32000  cnlnadjeu  32014  poimirlem25  37646  poimirlem26  37647  hdmap1eulem  41823  hdmap1eulemOLDN  41824  hdmap14lem6  41874  reuf1odnf  47112  euoreqb  47114  isuspgrim0  47898  isuspgrimlem  47899  joindm3  48961  meetdm3  48963  upciclem1  49159  upfval2  49170  upfval3  49171  isuplem  49172  oppcup3lem  49199  isinito2lem  49491