Theorem reubidv 3372

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

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

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 2533  df-eu 2562  df-reu 3355

This theorem is referenced by:  reueqd  3392  sbcreu  3839  oawordeu  8519  xpf1o  9103  dfac2b  10084  creur  12180  creui  12181  divalg  16373  divalg2  16375  lubfval  18309  lubeldm  18312  lubval  18315  glbfval  18322  glbeldm  18325  glbval  18328  joineu  18341  meeteu  18355  dfod2  19494  ustuqtop  24134  addsq2reu  27351  addsqn2reu  27352  addsqrexnreu  27353  addsqnreup  27354  2sqreulem1  27357  2sqreunnlem1  27360  usgredg2vtxeuALT  29149  isfrgr  30189  frcond1  30195  frgr1v  30200  nfrgr2v  30201  frgr3v  30204  3vfriswmgr  30207  n4cyclfrgr  30220  eulplig  30414  riesz4  31993  cnlnadjeu  32007  poimirlem25  37639  poimirlem26  37640  hdmap1eulem  41816  hdmap1eulemOLDN  41817  hdmap14lem6  41867  reuf1odnf  47108  euoreqb  47110  isuspgrim0  47894  isuspgrimlem  47895  joindm3  48957  meetdm3  48959  upciclem1  49155  upfval2  49166  upfval3  49167  isuplem  49168  oppcup3lem  49195  isinito2lem  49487