Theorem reubidv 3362

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2111  ∃!wreu 3344

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 2535  df-eu 2564  df-reu 3347

This theorem is referenced by:  reueqd  3382  sbcreu  3827  oawordeu  8470  xpf1o  9052  dfac2b  10019  creur  12116  creui  12117  divalg  16311  divalg2  16313  lubfval  18251  lubeldm  18254  lubval  18257  glbfval  18264  glbeldm  18267  glbval  18270  joineu  18283  meeteu  18297  dfod2  19474  ustuqtop  24159  addsq2reu  27376  addsqn2reu  27377  addsqrexnreu  27378  addsqnreup  27379  2sqreulem1  27382  2sqreunnlem1  27385  usgredg2vtxeuALT  29198  isfrgr  30235  frcond1  30241  frgr1v  30246  nfrgr2v  30247  frgr3v  30250  3vfriswmgr  30253  n4cyclfrgr  30266  eulplig  30460  riesz4  32039  cnlnadjeu  32053  poimirlem25  37684  poimirlem26  37685  hdmap1eulem  41860  hdmap1eulemOLDN  41861  hdmap14lem6  41911  reuf1odnf  47137  euoreqb  47139  isuspgrim0  47924  isuspgrimlem  47925  joindm3  48999  meetdm3  49001  upciclem1  49197  upfval2  49208  upfval3  49209  isuplem  49210  oppcup3lem  49237  isinito2lem  49529