Theorem reubidv 3383

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

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

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 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2566  df-eu 2596  df-reu 3368

This theorem is used by:  reueqd  3401  sbcreu  3826  oawordeu  8546  xpf1o  9141  dfac2b  10137  creur  12240  creui  12241  divalg  16499  divalg2  16501  lubfval  18442  lubeldm  18445  lubval  18448  glbfval  18455  glbeldm  18458  glbval  18461  joineu  18474  meeteu  18488  dfod2  19697  ustuqtop  24478  addsq2reu  27684  addsqn2reu  27685  addsqrexnreu  27686  addsqnreup  27687  2sqreulem1  27690  2sqreunnlem1  27693  angmgmaddov1  29275  angmgmaddov2  29276  usgredg2vtxeuALT  29690  isfrgr  30748  frcond1  30754  frgr1v  30759  nfrgr2v  30760  frgr3v  30763  3vfriswmgr  30766  n4cyclfrgr  30779  eulplig  30974  riesz4  32553  cnlnadjeu  32567  poimirlem25  38402  poimirlem26  38403  hdmap1eulem  42703  hdmap1eulemOLDN  42704  hdmap14lem6  42754  reuf1odnf  48003  euoreqb  48005  isuspgrim0  48818  isuspgrimlem  48819  joindm3  49903  meetdm3  49905  upciclem1  50100  upfval2  50111  upfval3  50112  isuplem  50113  oppcup3lem  50140  isinito2lem  50432