Theorem reubidv 3366

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ∃!wreu 3348

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  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539  df-eu 2569  df-reu 3351

This theorem is referenced by:  reueqd  3386  sbcreu  3826  oawordeu  8482  xpf1o  9067  dfac2b  10041  creur  12139  creui  12140  divalg  16330  divalg2  16332  lubfval  18271  lubeldm  18274  lubval  18277  glbfval  18284  glbeldm  18287  glbval  18290  joineu  18303  meeteu  18317  dfod2  19493  ustuqtop  24190  addsq2reu  27407  addsqn2reu  27408  addsqrexnreu  27409  addsqnreup  27410  2sqreulem1  27413  2sqreunnlem1  27416  usgredg2vtxeuALT  29295  isfrgr  30335  frcond1  30341  frgr1v  30346  nfrgr2v  30347  frgr3v  30350  3vfriswmgr  30353  n4cyclfrgr  30366  eulplig  30560  riesz4  32139  cnlnadjeu  32153  poimirlem25  37842  poimirlem26  37843  hdmap1eulem  42078  hdmap1eulemOLDN  42079  hdmap14lem6  42129  reuf1odnf  47349  euoreqb  47351  isuspgrim0  48136  isuspgrimlem  48137  joindm3  49210  meetdm3  49212  upciclem1  49407  upfval2  49418  upfval3  49419  isuplem  49420  oppcup3lem  49447  isinito2lem  49739