Theorem reubidv 3389

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2099  ∃!wreu 3369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-mo 2529  df-eu 2558  df-reu 3372

This theorem is referenced by:  reueqd  3414  sbcreu  3866  oawordeu  8569  xpf1o  9155  dfac2b  10145  creur  12228  creui  12229  divalg  16371  divalg2  16373  lubfval  18333  lubeldm  18336  lubval  18339  glbfval  18346  glbeldm  18349  glbval  18352  joineu  18365  meeteu  18379  dfod2  19510  ustuqtop  24138  addsq2reu  27360  addsqn2reu  27361  addsqrexnreu  27362  addsqnreup  27363  2sqreulem1  27366  2sqreunnlem1  27369  usgredg2vtxeuALT  29022  isfrgr  30057  frcond1  30063  frgr1v  30068  nfrgr2v  30069  frgr3v  30072  3vfriswmgr  30075  n4cyclfrgr  30088  eulplig  30282  riesz4  31861  cnlnadjeu  31875  poimirlem25  37053  poimirlem26  37054  hdmap1eulem  41232  hdmap1eulemOLDN  41233  hdmap14lem6  41283  reuf1odnf  46410  euoreqb  46412  isuspgrim0  47093  isuspgrimlem  47095  joindm3  47911  meetdm3  47913