Theorem reubidv 3395

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2105  ∃!wreu 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-mo 2537  df-eu 2566  df-reu 3378

This theorem is referenced by:  reueqd  3418  sbcreu  3884  oawordeu  8591  xpf1o  9177  dfac2b  10168  creur  12257  creui  12258  divalg  16436  divalg2  16438  lubfval  18407  lubeldm  18410  lubval  18413  glbfval  18420  glbeldm  18423  glbval  18426  joineu  18439  meeteu  18453  dfod2  19596  ustuqtop  24270  addsq2reu  27498  addsqn2reu  27499  addsqrexnreu  27500  addsqnreup  27501  2sqreulem1  27504  2sqreunnlem1  27507  usgredg2vtxeuALT  29253  isfrgr  30288  frcond1  30294  frgr1v  30299  nfrgr2v  30300  frgr3v  30303  3vfriswmgr  30306  n4cyclfrgr  30319  eulplig  30513  riesz4  32092  cnlnadjeu  32106  poimirlem25  37631  poimirlem26  37632  hdmap1eulem  41804  hdmap1eulemOLDN  41805  hdmap14lem6  41855  reuf1odnf  47056  euoreqb  47058  isuspgrim0  47809  isuspgrimlem  47811  joindm3  48765  meetdm3  48767  upciclem1  48811