Theorem reubidv 3406

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543  df-eu 2572  df-reu 3389

This theorem is referenced by:  reueqd  3430  sbcreu  3898  oawordeu  8611  xpf1o  9205  dfac2b  10200  creur  12287  creui  12288  divalg  16451  divalg2  16453  lubfval  18420  lubeldm  18423  lubval  18426  glbfval  18433  glbeldm  18436  glbval  18439  joineu  18452  meeteu  18466  dfod2  19606  ustuqtop  24276  addsq2reu  27502  addsqn2reu  27503  addsqrexnreu  27504  addsqnreup  27505  2sqreulem1  27508  2sqreunnlem1  27511  usgredg2vtxeuALT  29257  isfrgr  30292  frcond1  30298  frgr1v  30303  nfrgr2v  30304  frgr3v  30307  3vfriswmgr  30310  n4cyclfrgr  30323  eulplig  30517  riesz4  32096  cnlnadjeu  32110  poimirlem25  37605  poimirlem26  37606  hdmap1eulem  41779  hdmap1eulemOLDN  41780  hdmap14lem6  41830  reuf1odnf  47022  euoreqb  47024  isuspgrim0  47756  isuspgrimlem  47758  joindm3  48649  meetdm3  48651