Theorem reubidv 3126

Description: Formula-building rule for restricted existential quantifier (deduction rule). (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 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3125	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 1990  ∃!wreu 2914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710  df-eu 2474  df-reu 2919

This theorem is referenced by:  reueqd  3148  sbcreu  3515  oawordeu  7635  xpf1o  8122  dfac2  8953  creur  11014  creui  11015  divalg  15126  divalg2  15128  lubfval  16978  lubeldm  16981  lubval  16984  glbfval  16991  glbeldm  16994  glbval  16997  joineu  17010  meeteu  17024  dfod2  17981  ustuqtop  22050  usgredg2vtxeuALT  26114  isfrgr  27122  frcond1  27130  frgr1v  27135  nfrgr2v  27136  frgr3v  27139  3vfriswmgr  27142  n4cyclfrgr  27155  eulplig  27337  riesz4  28923  cnlnadjeu  28937  poimirlem25  33434  poimirlem26  33435  hdmap1eulem  37113  hdmap1eulemOLDN  37114  hdmap14lem6  37165