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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147  ∃!wreu 3367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567  df-eu 2597  df-reu 3370

This theorem is used by:  reueqd  3403  sbcreu  3827  oawordeu  8594  xpf1o  9189  dfac2b  10239  creur  12344  creui  12345  divalg  16605  divalg2  16607  lubfval  18554  lubeldm  18557  lubval  18560  glbfval  18567  glbeldm  18570  glbval  18573  joineu  18586  meeteu  18600  dfod2  19811  ustuqtop  24598  addsq2reu  27800  addsqn2reu  27801  addsqrexnreu  27802  addsqnreup  27803  2sqreulem1  27806  2sqreunnlem1  27809  angmgmaddov1  29421  angmgmaddov2  29422  usgredg2vtxeuALT  29836  isfrgr  30894  frcond1  30900  frgr1v  30905  nfrgr2v  30906  frgr3v  30909  3vfriswmgr  30912  n4cyclfrgr  30925  eulplig  31120  riesz4  32699  cnlnadjeu  32713  poimirlem25  38768  poimirlem26  38769  hdmap1eulem  43082  hdmap1eulemOLDN  43083  hdmap14lem6  43133  reuf1odnf  48393  euoreqb  48395  isuspgrim0  49207  isuspgrimlem  49208  joindm3  50298  meetdm3  50300  upciclem1  50497  upfval2  50508  upfval3  50509  isuplem  50510  oppcup3lem  50537  isinito2lem  50848