Theorem reubidv 3389

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 483	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3388	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2110  ∃!wreu 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-mo 2618  df-eu 2650  df-reu 3145

This theorem is referenced by:  reueqd  3419  sbcreu  3858  oawordeu  8180  xpf1o  8678  dfac2b  9555  creur  11631  creui  11632  divalg  15753  divalg2  15755  lubfval  17587  lubeldm  17590  lubval  17593  glbfval  17600  glbeldm  17603  glbval  17606  joineu  17619  meeteu  17633  dfod2  18690  ustuqtop  22854  addsq2reu  26015  addsqn2reu  26016  addsqrexnreu  26017  addsqnreup  26018  2sqreulem1  26021  2sqreunnlem1  26024  usgredg2vtxeuALT  27003  isfrgr  28038  frcond1  28044  frgr1v  28049  nfrgr2v  28050  frgr3v  28053  3vfriswmgr  28056  n4cyclfrgr  28069  eulplig  28261  riesz4  29840  cnlnadjeu  29854  poimirlem25  34916  poimirlem26  34917  hdmap1eulem  38957  hdmap1eulemOLDN  38958  hdmap14lem6  39008  reuf1odnf  43305  euoreqb  43307