Theorem reubidv 3368

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∃!wreu 3350

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-reu 3353

This theorem is referenced by:  reueqd  3388  sbcreu  3828  oawordeu  8492  xpf1o  9079  dfac2b  10053  creur  12151  creui  12152  divalg  16342  divalg2  16344  lubfval  18283  lubeldm  18286  lubval  18289  glbfval  18296  glbeldm  18299  glbval  18302  joineu  18315  meeteu  18329  dfod2  19505  ustuqtop  24202  addsq2reu  27419  addsqn2reu  27420  addsqrexnreu  27421  addsqnreup  27422  2sqreulem1  27425  2sqreunnlem1  27428  usgredg2vtxeuALT  29307  isfrgr  30347  frcond1  30353  frgr1v  30358  nfrgr2v  30359  frgr3v  30362  3vfriswmgr  30365  n4cyclfrgr  30378  eulplig  30572  riesz4  32151  cnlnadjeu  32165  poimirlem25  37890  poimirlem26  37891  hdmap1eulem  42192  hdmap1eulemOLDN  42193  hdmap14lem6  42243  reuf1odnf  47461  euoreqb  47463  isuspgrim0  48248  isuspgrimlem  48249  joindm3  49322  meetdm3  49324  upciclem1  49519  upfval2  49530  upfval3  49531  isuplem  49532  oppcup3lem  49559  isinito2lem  49851