Theorem reubidv 3301

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)

Hypothesis

Ref	Expression
reubidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
reubidv	⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidv

Step	Hyp	Ref	Expression
1		reubidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 484	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3300	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2110  ∃!wreu 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-mo 2539  df-eu 2568  df-reu 3068

This theorem is referenced by:  reueqd  3327  sbcreu  3788  oawordeu  8283  xpf1o  8808  dfac2b  9744  creur  11824  creui  11825  divalg  15964  divalg2  15966  lubfval  17856  lubeldm  17859  lubval  17862  glbfval  17869  glbeldm  17872  glbval  17875  joineu  17888  meeteu  17902  dfod2  18955  ustuqtop  23144  addsq2reu  26321  addsqn2reu  26322  addsqrexnreu  26323  addsqnreup  26324  2sqreulem1  26327  2sqreunnlem1  26330  usgredg2vtxeuALT  27310  isfrgr  28343  frcond1  28349  frgr1v  28354  nfrgr2v  28355  frgr3v  28358  3vfriswmgr  28361  n4cyclfrgr  28374  eulplig  28566  riesz4  30145  cnlnadjeu  30159  poimirlem25  35539  poimirlem26  35540  hdmap1eulem  39573  hdmap1eulemOLDN  39574  hdmap14lem6  39624  reuf1odnf  44271  euoreqb  44273  joindm3  45936  meetdm3  45938