Theorem reubidva 3393

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 579	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	eubidv 2583	. 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-reu 3378	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-reu 3378	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2105  ∃!weu 2565  ∃!wreu 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-mo 2537  df-eu 2566  df-reu 3378

This theorem is referenced by:  reubidv  3395  reuxfrd  3756  reuxfr1d  3758  fdmeu  6964  exfo  7124  f1ofveu  7424  zmax  12984  zbtwnre  12985  rebtwnz  12986  icoshftf1o  13510  divalgb  16437  1arith2  16961  ply1divalg2  26192  addsq2reu  27498  addsqn2reu  27499  addsqrexnreu  27500  2sqreultlem  27505  2sqreunnltlem  27508  frgr2wwlkeu  30355  numclwwlk2lem1  30404  numclwlk2lem2f1o  30407  pjhtheu2  31444  reuxfrdf  32518  xrsclat  32995  xrmulc1cn  33890  ply1divalg3  35626  poimirlem25  37631  hdmap14lem14  41863  cantnf2  43314  prproropreud  47433  quad1  47544  requad1  47546  requad2  47547  isuspgrim0lem  47808  isuspgrim0  47809  isuspgrimlem  47811  itscnhlinecirc02p  48634  reuxfr1dd  48654