Theorem reubidv 3386

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2145  ∃!wreu 3368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-mo 2569  df-eu 2599  df-reu 3371

This theorem is referenced by:  reueqd  3404  sbcreu  3832  oawordeu  8528  xpf1o  9115  dfac2b  10102  creur  12203  creui  12204  divalg  16451  divalg2  16453  lubfval  18394  lubeldm  18397  lubval  18400  glbfval  18407  glbeldm  18410  glbval  18413  joineu  18426  meeteu  18440  dfod2  19625  ustuqtop  24364  addsq2reu  27562  addsqn2reu  27563  addsqrexnreu  27564  addsqnreup  27565  2sqreulem1  27568  2sqreunnlem1  27571  usgredg2vtxeuALT  29481  isfrgr  30520  frcond1  30526  frgr1v  30531  nfrgr2v  30532  frgr3v  30535  3vfriswmgr  30538  n4cyclfrgr  30551  eulplig  30746  riesz4  32325  cnlnadjeu  32339  poimirlem25  38156  poimirlem26  38157  hdmap1eulem  42458  hdmap1eulemOLDN  42459  hdmap14lem6  42509  reuf1odnf  47699  euoreqb  47701  isuspgrim0  48514  isuspgrimlem  48515  joindm3  49598  meetdm3  49600  upciclem1  49795  upfval2  49806  upfval3  49807  isuplem  49808  oppcup3lem  49835  isinito2lem  50127