Theorem reubidv 3335

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

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

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 398  df-ex 1780  df-mo 2538  df-eu 2567  df-reu 3286

This theorem is referenced by:  reueqd  3362  sbcreu  3814  oawordeu  8417  xpf1o  8964  dfac2b  9932  creur  12013  creui  12014  divalg  16157  divalg2  16159  lubfval  18113  lubeldm  18116  lubval  18119  glbfval  18126  glbeldm  18129  glbval  18132  joineu  18145  meeteu  18159  dfod2  19216  ustuqtop  23443  addsq2reu  26633  addsqn2reu  26634  addsqrexnreu  26635  addsqnreup  26636  2sqreulem1  26639  2sqreunnlem1  26642  usgredg2vtxeuALT  27634  isfrgr  28669  frcond1  28675  frgr1v  28680  nfrgr2v  28681  frgr3v  28684  3vfriswmgr  28687  n4cyclfrgr  28700  eulplig  28892  riesz4  30471  cnlnadjeu  30485  poimirlem25  35846  poimirlem26  35847  hdmap1eulem  39878  hdmap1eulemOLDN  39879  hdmap14lem6  39929  reuf1odnf  44657  euoreqb  44659  joindm3  46321  meetdm3  46323