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 2113  ∃!wreu 3345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  reueqd  3383  sbcreu  3823  oawordeu  8476  xpf1o  9059  dfac2b  10029  creur  12126  creui  12127  divalg  16316  divalg2  16318  lubfval  18256  lubeldm  18259  lubval  18262  glbfval  18269  glbeldm  18272  glbval  18275  joineu  18288  meeteu  18302  dfod2  19478  ustuqtop  24162  addsq2reu  27379  addsqn2reu  27380  addsqrexnreu  27381  addsqnreup  27382  2sqreulem1  27385  2sqreunnlem1  27388  usgredg2vtxeuALT  29202  isfrgr  30242  frcond1  30248  frgr1v  30253  nfrgr2v  30254  frgr3v  30257  3vfriswmgr  30260  n4cyclfrgr  30273  eulplig  30467  riesz4  32046  cnlnadjeu  32060  poimirlem25  37705  poimirlem26  37706  hdmap1eulem  41941  hdmap1eulemOLDN  41942  hdmap14lem6  41992  reuf1odnf  47231  euoreqb  47233  isuspgrim0  48018  isuspgrimlem  48019  joindm3  49093  meetdm3  49095  upciclem1  49291  upfval2  49302  upfval3  49303  isuplem  49304  oppcup3lem  49331  isinito2lem  49623