Theorem reubidv 3385

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 485	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3383	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2143  ∃!wreu 3367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597  df-reu 3370

This theorem is referenced by:  reueqd  3403  sbcreu  3830  oawordeu  8541  xpf1o  9128  dfac2b  10115  creur  12213  creui  12214  divalg  16462  divalg2  16464  lubfval  18405  lubeldm  18408  lubval  18411  glbfval  18418  glbeldm  18421  glbval  18424  joineu  18437  meeteu  18451  dfod2  19635  ustuqtop  24384  addsq2reu  27582  addsqn2reu  27583  addsqrexnreu  27584  addsqnreup  27585  2sqreulem1  27588  2sqreunnlem1  27591  usgredg2vtxeuALT  29550  isfrgr  30589  frcond1  30595  frgr1v  30600  nfrgr2v  30601  frgr3v  30604  3vfriswmgr  30607  n4cyclfrgr  30620  eulplig  30815  riesz4  32394  cnlnadjeu  32408  poimirlem25  38274  poimirlem26  38275  hdmap1eulem  42574  hdmap1eulemOLDN  42575  hdmap14lem6  42625  reuf1odnf  47821  euoreqb  47823  isuspgrim0  48636  isuspgrimlem  48637  joindm3  49724  meetdm3  49726  upciclem1  49921  upfval2  49932  upfval3  49933  isuplem  49934  oppcup3lem  49961  isinito2lem  50253