Theorem reubidv 3321

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2109  ∃!wreu 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-mo 2541  df-eu 2570  df-reu 3072

This theorem is referenced by:  reueqd  3348  sbcreu  3813  oawordeu  8362  xpf1o  8891  dfac2b  9870  creur  11950  creui  11951  divalg  16093  divalg2  16095  lubfval  18049  lubeldm  18052  lubval  18055  glbfval  18062  glbeldm  18065  glbval  18068  joineu  18081  meeteu  18095  dfod2  19152  ustuqtop  23379  addsq2reu  26569  addsqn2reu  26570  addsqrexnreu  26571  addsqnreup  26572  2sqreulem1  26575  2sqreunnlem1  26578  usgredg2vtxeuALT  27570  isfrgr  28603  frcond1  28609  frgr1v  28614  nfrgr2v  28615  frgr3v  28618  3vfriswmgr  28621  n4cyclfrgr  28634  eulplig  28826  riesz4  30405  cnlnadjeu  30419  poimirlem25  35781  poimirlem26  35782  hdmap1eulem  39815  hdmap1eulemOLDN  39816  hdmap14lem6  39866  reuf1odnf  44550  euoreqb  44552  joindm3  46215  meetdm3  46217