Theorem reubidv 3363

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

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

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 3346

This theorem is referenced by:  reueqd  3383  sbcreu  3830  oawordeu  8480  xpf1o  9063  dfac2b  10044  creur  12140  creui  12141  divalg  16332  divalg2  16334  lubfval  18272  lubeldm  18275  lubval  18278  glbfval  18285  glbeldm  18288  glbval  18291  joineu  18304  meeteu  18318  dfod2  19461  ustuqtop  24150  addsq2reu  27367  addsqn2reu  27368  addsqrexnreu  27369  addsqnreup  27370  2sqreulem1  27373  2sqreunnlem1  27376  usgredg2vtxeuALT  29185  isfrgr  30222  frcond1  30228  frgr1v  30233  nfrgr2v  30234  frgr3v  30237  3vfriswmgr  30240  n4cyclfrgr  30253  eulplig  30447  riesz4  32026  cnlnadjeu  32040  poimirlem25  37624  poimirlem26  37625  hdmap1eulem  41801  hdmap1eulemOLDN  41802  hdmap14lem6  41852  reuf1odnf  47092  euoreqb  47094  isuspgrim0  47878  isuspgrimlem  47879  joindm3  48941  meetdm3  48943  upciclem1  49139  upfval2  49150  upfval3  49151  isuplem  49152  oppcup3lem  49179  isinito2lem  49471