Theorem reubidv 3358

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∃!wreu 3340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2539  df-eu 2569  df-reu 3343

This theorem is referenced by:  reueqd  3376  sbcreu  3814  oawordeu  8490  xpf1o  9077  dfac2b  10053  creur  12153  creui  12154  divalg  16372  divalg2  16374  lubfval  18314  lubeldm  18317  lubval  18320  glbfval  18327  glbeldm  18330  glbval  18333  joineu  18346  meeteu  18360  dfod2  19539  ustuqtop  24211  addsq2reu  27403  addsqn2reu  27404  addsqrexnreu  27405  addsqnreup  27406  2sqreulem1  27409  2sqreunnlem1  27412  usgredg2vtxeuALT  29291  isfrgr  30330  frcond1  30336  frgr1v  30341  nfrgr2v  30342  frgr3v  30345  3vfriswmgr  30348  n4cyclfrgr  30361  eulplig  30556  riesz4  32135  cnlnadjeu  32149  poimirlem25  37966  poimirlem26  37967  hdmap1eulem  42268  hdmap1eulemOLDN  42269  hdmap14lem6  42319  reuf1odnf  47555  euoreqb  47557  isuspgrim0  48370  isuspgrimlem  48371  joindm3  49444  meetdm3  49446  upciclem1  49641  upfval2  49652  upfval3  49653  isuplem  49654  oppcup3lem  49681  isinito2lem  49973