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  37846  poimirlem26  37847  hdmap1eulem  42082  hdmap1eulemOLDN  42083  hdmap14lem6  42133  reuf1odnf  47353  euoreqb  47355  isuspgrim0  48140  isuspgrimlem  48141  joindm3  49214  meetdm3  49216  upciclem1  49411  upfval2  49422  upfval3  49423  isuplem  49424  oppcup3lem  49451  isinito2lem  49743