Theorem reubidv 3382

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2141  ∃!wreu 3364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-mo 2565  df-eu 2595  df-reu 3367

This theorem is referenced by:  reueqd  3400  sbcreu  3829  oawordeu  8519  xpf1o  9107  dfac2b  10084  creur  12186  creui  12187  divalg  16420  divalg2  16422  lubfval  18363  lubeldm  18366  lubval  18369  glbfval  18376  glbeldm  18379  glbval  18382  joineu  18395  meeteu  18409  dfod2  19587  ustuqtop  24286  addsq2reu  27481  addsqn2reu  27482  addsqrexnreu  27483  addsqnreup  27484  2sqreulem1  27487  2sqreunnlem1  27490  usgredg2vtxeuALT  29369  isfrgr  30408  frcond1  30414  frgr1v  30419  nfrgr2v  30420  frgr3v  30423  3vfriswmgr  30426  n4cyclfrgr  30439  eulplig  30634  riesz4  32213  cnlnadjeu  32227  poimirlem25  38108  poimirlem26  38109  hdmap1eulem  42410  hdmap1eulemOLDN  42411  hdmap14lem6  42461  reuf1odnf  47665  euoreqb  47667  isuspgrim0  48480  isuspgrimlem  48481  joindm3  49554  meetdm3  49556  upciclem1  49751  upfval2  49762  upfval3  49763  isuplem  49764  oppcup3lem  49791  isinito2lem  50083