Theorem reubidv 3377

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

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

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 2539  df-eu 2568  df-reu 3360

This theorem is referenced by:  reueqd  3400  sbcreu  3851  oawordeu  8567  xpf1o  9153  dfac2b  10145  creur  12234  creui  12235  divalg  16422  divalg2  16424  lubfval  18360  lubeldm  18363  lubval  18366  glbfval  18373  glbeldm  18376  glbval  18379  joineu  18392  meeteu  18406  dfod2  19545  ustuqtop  24185  addsq2reu  27403  addsqn2reu  27404  addsqrexnreu  27405  addsqnreup  27406  2sqreulem1  27409  2sqreunnlem1  27412  usgredg2vtxeuALT  29201  isfrgr  30241  frcond1  30247  frgr1v  30252  nfrgr2v  30253  frgr3v  30256  3vfriswmgr  30259  n4cyclfrgr  30272  eulplig  30466  riesz4  32045  cnlnadjeu  32059  poimirlem25  37669  poimirlem26  37670  hdmap1eulem  41841  hdmap1eulemOLDN  41842  hdmap14lem6  41892  reuf1odnf  47136  euoreqb  47138  isuspgrim0  47907  isuspgrimlem  47908  joindm3  48943  meetdm3  48945  upciclem1  49101  upfval2  49112  upfval3  49113  isuplem  49114  oppcup3lem  49139  isinito2lem  49383