Theorem reubidv 3322

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

Syntax hints:   → wi 4   ↔ wb 198   ∈ wcel 2051  ∃!wreu 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-mo 2548  df-eu 2585  df-reu 3088

This theorem is referenced by:  reueqd  3352  sbcreu  3755  oawordeu  7980  xpf1o  8473  dfac2b  9348  creur  11431  creui  11432  divalg  15612  divalg2  15614  lubfval  17458  lubeldm  17461  lubval  17464  glbfval  17471  glbeldm  17474  glbval  17477  joineu  17490  meeteu  17504  dfod2  18464  ustuqtop  22573  addsq2reu  25733  addsqn2reu  25734  addsqrexnreu  25735  addsqnreup  25736  2sqreulem1  25739  2sqreunnlem1  25742  usgredg2vtxeuALT  26722  isfrgr  27807  frcond1  27815  frgr1v  27820  nfrgr2v  27821  frgr3v  27824  3vfriswmgr  27827  n4cyclfrgr  27840  eulplig  28054  riesz4  29637  cnlnadjeu  29651  poimirlem25  34395  poimirlem26  34396  hdmap1eulem  38440  hdmap1eulemOLDN  38441  hdmap14lem6  38491  reuf1odnf  42746  euoreqb  42748