Theorem reubidv 3392

Description: Formula-building rule for restricted existential 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 479	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3390	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2104  ∃!wreu 3372

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-mo 2532  df-eu 2561  df-reu 3375

This theorem is referenced by:  reueqd  3417  sbcreu  3869  oawordeu  8557  xpf1o  9141  dfac2b  10127  creur  12210  creui  12211  divalg  16350  divalg2  16352  lubfval  18307  lubeldm  18310  lubval  18313  glbfval  18320  glbeldm  18323  glbval  18326  joineu  18339  meeteu  18353  dfod2  19473  ustuqtop  23971  addsq2reu  27179  addsqn2reu  27180  addsqrexnreu  27181  addsqnreup  27182  2sqreulem1  27185  2sqreunnlem1  27188  usgredg2vtxeuALT  28746  isfrgr  29780  frcond1  29786  frgr1v  29791  nfrgr2v  29792  frgr3v  29795  3vfriswmgr  29798  n4cyclfrgr  29811  eulplig  30005  riesz4  31584  cnlnadjeu  31598  poimirlem25  36816  poimirlem26  36817  hdmap1eulem  40996  hdmap1eulemOLDN  40997  hdmap14lem6  41047  reuf1odnf  46113  euoreqb  46115  joindm3  47689  meetdm3  47691