Theorem reubidv 3382

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 3380	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2098  ∃!wreu 3362

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-mo 2528  df-eu 2557  df-reu 3365

This theorem is referenced by:  reueqd  3406  sbcreu  3867  oawordeu  8574  xpf1o  9162  dfac2b  10153  creur  12236  creui  12237  divalg  16379  divalg2  16381  lubfval  18341  lubeldm  18344  lubval  18347  glbfval  18354  glbeldm  18357  glbval  18360  joineu  18373  meeteu  18387  dfod2  19523  ustuqtop  24181  addsq2reu  27403  addsqn2reu  27404  addsqrexnreu  27405  addsqnreup  27406  2sqreulem1  27409  2sqreunnlem1  27412  usgredg2vtxeuALT  29091  isfrgr  30126  frcond1  30132  frgr1v  30137  nfrgr2v  30138  frgr3v  30141  3vfriswmgr  30144  n4cyclfrgr  30157  eulplig  30351  riesz4  31930  cnlnadjeu  31944  poimirlem25  37188  poimirlem26  37189  hdmap1eulem  41364  hdmap1eulemOLDN  41365  hdmap14lem6  41415  reuf1odnf  46550  euoreqb  46552  isuspgrim0  47282  isuspgrimlem  47284  joindm3  48100  meetdm3  48102