Theorem reubidv 3398

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∃!wreu 3378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-reu 3381

This theorem is referenced by:  reueqd  3421  sbcreu  3876  oawordeu  8593  xpf1o  9179  dfac2b  10171  creur  12260  creui  12261  divalg  16440  divalg2  16442  lubfval  18395  lubeldm  18398  lubval  18401  glbfval  18408  glbeldm  18411  glbval  18414  joineu  18427  meeteu  18441  dfod2  19582  ustuqtop  24255  addsq2reu  27484  addsqn2reu  27485  addsqrexnreu  27486  addsqnreup  27487  2sqreulem1  27490  2sqreunnlem1  27493  usgredg2vtxeuALT  29239  isfrgr  30279  frcond1  30285  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  3vfriswmgr  30297  n4cyclfrgr  30310  eulplig  30504  riesz4  32083  cnlnadjeu  32097  poimirlem25  37652  poimirlem26  37653  hdmap1eulem  41824  hdmap1eulemOLDN  41825  hdmap14lem6  41875  reuf1odnf  47119  euoreqb  47121  isuspgrim0  47872  isuspgrimlem  47874  joindm3  48866  meetdm3  48868  upciclem1  48923  upfval2  48934  upfval3  48935  isuplem  48936