Theorem reubidv 3395

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  ∃!wreu 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535  df-eu 2564  df-reu 3378

This theorem is referenced by:  reueqd  3420  sbcreu  3871  oawordeu  8555  xpf1o  9139  dfac2b  10125  creur  12206  creui  12207  divalg  16346  divalg2  16348  lubfval  18303  lubeldm  18306  lubval  18309  glbfval  18316  glbeldm  18319  glbval  18322  joineu  18335  meeteu  18349  dfod2  19432  ustuqtop  23751  addsq2reu  26943  addsqn2reu  26944  addsqrexnreu  26945  addsqnreup  26946  2sqreulem1  26949  2sqreunnlem1  26952  usgredg2vtxeuALT  28479  isfrgr  29513  frcond1  29519  frgr1v  29524  nfrgr2v  29525  frgr3v  29528  3vfriswmgr  29531  n4cyclfrgr  29544  eulplig  29738  riesz4  31317  cnlnadjeu  31331  poimirlem25  36513  poimirlem26  36514  hdmap1eulem  40693  hdmap1eulemOLDN  40694  hdmap14lem6  40744  reuf1odnf  45815  euoreqb  45817  joindm3  47602  meetdm3  47604