Theorem reubidv 3359

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∃!wreu 3341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-reu 3344

This theorem is referenced by:  reueqd  3377  sbcreu  3815  oawordeu  8483  xpf1o  9070  dfac2b  10044  creur  12144  creui  12145  divalg  16363  divalg2  16365  lubfval  18305  lubeldm  18308  lubval  18311  glbfval  18318  glbeldm  18321  glbval  18324  joineu  18337  meeteu  18351  dfod2  19530  ustuqtop  24221  addsq2reu  27417  addsqn2reu  27418  addsqrexnreu  27419  addsqnreup  27420  2sqreulem1  27423  2sqreunnlem1  27426  usgredg2vtxeuALT  29305  isfrgr  30345  frcond1  30351  frgr1v  30356  nfrgr2v  30357  frgr3v  30360  3vfriswmgr  30363  n4cyclfrgr  30376  eulplig  30571  riesz4  32150  cnlnadjeu  32164  poimirlem25  37980  poimirlem26  37981  hdmap1eulem  42282  hdmap1eulemOLDN  42283  hdmap14lem6  42333  reuf1odnf  47567  euoreqb  47569  isuspgrim0  48382  isuspgrimlem  48383  joindm3  49456  meetdm3  49458  upciclem1  49653  upfval2  49664  upfval3  49665  isuplem  49666  oppcup3lem  49693  isinito2lem  49985