Theorem reubidv 3393

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)

Hypothesis

Ref	Expression
rmobidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
reubidv	⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidv

Step	Hyp	Ref	Expression
1		rmobidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3391	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ∃!wreu 3373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2533  df-eu 2562  df-reu 3376

This theorem is referenced by:  reueqd  3418  sbcreu  3866  oawordeu  8538  xpf1o  9122  dfac2b  10107  creur  12188  creui  12189  divalg  16328  divalg2  16330  lubfval  18285  lubeldm  18288  lubval  18291  glbfval  18298  glbeldm  18301  glbval  18304  joineu  18317  meeteu  18331  dfod2  19396  ustuqtop  23680  addsq2reu  26870  addsqn2reu  26871  addsqrexnreu  26872  addsqnreup  26873  2sqreulem1  26876  2sqreunnlem1  26879  usgredg2vtxeuALT  28344  isfrgr  29378  frcond1  29384  frgr1v  29389  nfrgr2v  29390  frgr3v  29393  3vfriswmgr  29396  n4cyclfrgr  29409  eulplig  29601  riesz4  31180  cnlnadjeu  31194  poimirlem25  36317  poimirlem26  36318  hdmap1eulem  40498  hdmap1eulemOLDN  40499  hdmap14lem6  40549  reuf1odnf  45587  euoreqb  45589  joindm3  47250  meetdm3  47252