Theorem reubidva 3361

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∃!weu 2561  ∃!wreu 3343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-eu 2562  df-reu 3346

This theorem is referenced by:  reubidv  3363  reuxfrd  3710  reuxfr1d  3712  fdmeu  6883  exfo  7043  f1ofveu  7347  zmax  12864  zbtwnre  12865  rebtwnz  12866  icoshftf1o  13395  divalgb  16333  1arith2  16858  ply1divalg2  26060  addsq2reu  27367  addsqn2reu  27368  addsqrexnreu  27369  2sqreultlem  27374  2sqreunnltlem  27377  frgr2wwlkeu  30289  numclwwlk2lem1  30338  numclwlk2lem2f1o  30341  pjhtheu2  31378  reuxfrdf  32453  xrsclat  32978  xrmulc1cn  33899  ply1divalg3  35617  poimirlem25  37627  hdmap14lem14  41863  cantnf2  43301  prproropreud  47497  quad1  47608  requad1  47610  requad2  47611  isuspgrim0lem  47881  isuspgrim0  47882  isuspgrimlem  47883  itscnhlinecirc02p  48774  reueqbidva  48794  reuxfr1dd  48795  uptrlem1  49199  isinito2lem  49487  lanup  49630  ranup  49631  islmd  49654  iscmd  49655