Theorem reubidv 3156

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

Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 2030  ∃!wreu 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750  df-eu 2502  df-reu 2948

This theorem is referenced by:  reueqd  3178  sbcreu  3548  oawordeu  7680  xpf1o  8163  dfac2  8991  creur  11052  creui  11053  divalg  15173  divalg2  15175  lubfval  17025  lubeldm  17028  lubval  17031  glbfval  17038  glbeldm  17041  glbval  17044  joineu  17057  meeteu  17071  dfod2  18027  ustuqtop  22097  usgredg2vtxeuALT  26159  isfrgr  27238  frcond1  27246  frgr1v  27251  nfrgr2v  27252  frgr3v  27255  3vfriswmgr  27258  n4cyclfrgr  27271  eulplig  27467  riesz4  29051  cnlnadjeu  29065  poimirlem25  33564  poimirlem26  33565  hdmap1eulem  37430  hdmap1eulemOLDN  37431  hdmap14lem6  37482