Theorem reubidv 3382

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

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

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 2565  df-eu 2595  df-reu 3367

This theorem is used by:  reueqd  3400  sbcreu  3823  oawordeu  8547  xpf1o  9142  dfac2b  10190  creur  12295  creui  12296  divalg  16553  divalg2  16555  lubfval  18502  lubeldm  18505  lubval  18508  glbfval  18515  glbeldm  18518  glbval  18521  joineu  18534  meeteu  18548  dfod2  19758  ustuqtop  24545  addsq2reu  27749  addsqn2reu  27750  addsqrexnreu  27751  addsqnreup  27752  2sqreulem1  27755  2sqreunnlem1  27758  angmgmaddov1  29370  angmgmaddov2  29371  usgredg2vtxeuALT  29785  isfrgr  30843  frcond1  30849  frgr1v  30854  nfrgr2v  30855  frgr3v  30858  3vfriswmgr  30861  n4cyclfrgr  30874  eulplig  31069  riesz4  32648  cnlnadjeu  32662  poimirlem25  38531  poimirlem26  38532  hdmap1eulem  42847  hdmap1eulemOLDN  42848  hdmap14lem6  42898  reuf1odnf  48121  euoreqb  48123  isuspgrim0  48936  isuspgrimlem  48937  joindm3  50021  meetdm3  50023  upciclem1  50218  upfval2  50229  upfval3  50230  isuplem  50231  oppcup3lem  50258  isinito2lem  50550