Theorem reubidv 3361

Description: Formula-building rule for restricted existential uniqueness 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 3359	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119  ∃!wreu 3343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-eu 2573  df-reu 3346

This theorem is referenced by:  reueqd  3379  sbcreu  3815  oawordeu  8487  xpf1o  9074  dfac2b  10051  creur  12151  creui  12152  divalg  16370  divalg2  16372  lubfval  18312  lubeldm  18315  lubval  18318  glbfval  18325  glbeldm  18328  glbval  18331  joineu  18344  meeteu  18358  dfod2  19537  ustuqtop  24236  addsq2reu  27428  addsqn2reu  27429  addsqrexnreu  27430  addsqnreup  27431  2sqreulem1  27434  2sqreunnlem1  27437  usgredg2vtxeuALT  29316  isfrgr  30355  frcond1  30361  frgr1v  30366  nfrgr2v  30367  frgr3v  30370  3vfriswmgr  30373  n4cyclfrgr  30386  eulplig  30581  riesz4  32160  cnlnadjeu  32174  poimirlem25  38019  poimirlem26  38020  hdmap1eulem  42321  hdmap1eulemOLDN  42322  hdmap14lem6  42372  reuf1odnf  47577  euoreqb  47579  isuspgrim0  48392  isuspgrimlem  48393  joindm3  49466  meetdm3  49468  upciclem1  49663  upfval2  49674  upfval3  49675  isuplem  49676  oppcup3lem  49703  isinito2lem  49995