Theorem reubidva 3385

Description: Formula-building rule for restricted existential uniqueness quantifier (deduction form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023.)

Hypothesis

Ref	Expression
rmobidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reubidva

Step	Hyp	Ref	Expression
1		rmobidva.1	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 590	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	eubidv 2616	. 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-reu 3372	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-reu 3372	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  ∃!weu 2598  ∃!wreu 3369

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2569  df-eu 2599  df-reu 3372

This theorem is used by:  reubidv  3387  reuxfrd  3713  reuxfr1d  3715  fdmeu  6941  exfo  7104  f1ofveu  7410  zmax  12981  zbtwnre  12982  rebtwnz  12983  icoshftf1o  13513  divalgb  16480  1arith2  17006  ply1divalg2  26327  addsq2reu  27635  addsqn2reu  27636  addsqrexnreu  27637  2sqreultlem  27642  2sqreunnltlem  27645  frgr2wwlkeu  30725  numclwwlk2lem1  30774  numclwlk2lem2f1o  30777  pjhtheu2  31815  reuxfrdf  32884  xrsclat  33371  xrmulc1cn  34360  ply1divalg3  36147  poimirlem25  38329  hdmap14lem14  42688  cantnf2  44085  prproropreud  48291  quad1  48418  requad1  48420  requad2  48421  isuspgrim0lem  48691  isuspgrim0  48692  isuspgrimlem  48693  itscnhlinecirc02p  49598  reueqbidva  49617  reuxfr1dd  49618  uptrlem1  50021  isinito2lem  50309  lanup  50452  ranup  50453  islmd  50476  iscmd  50477