Theorem reubidv 3388

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2108  ∃!wreu 3138

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 1905

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-mo 2616  df-eu 2648  df-reu 3143

This theorem is referenced by:  reueqd  3418  sbcreu  3857  oawordeu  8173  xpf1o  8671  dfac2b  9548  creur  11624  creui  11625  divalg  15746  divalg2  15748  lubfval  17580  lubeldm  17583  lubval  17586  glbfval  17593  glbeldm  17596  glbval  17599  joineu  17612  meeteu  17626  dfod2  18683  ustuqtop  22847  addsq2reu  26008  addsqn2reu  26009  addsqrexnreu  26010  addsqnreup  26011  2sqreulem1  26014  2sqreunnlem1  26017  usgredg2vtxeuALT  26996  isfrgr  28031  frcond1  28037  frgr1v  28042  nfrgr2v  28043  frgr3v  28046  3vfriswmgr  28049  n4cyclfrgr  28062  eulplig  28254  riesz4  29833  cnlnadjeu  29847  poimirlem25  34909  poimirlem26  34910  hdmap1eulem  38950  hdmap1eulemOLDN  38951  hdmap14lem6  39001  reuf1odnf  43296  euoreqb  43298