Theorem reubidva 3370

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

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

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 3355

This theorem is referenced by:  reubidv  3372  reuxfrd  3719  reuxfr1d  3721  fdmeu  6917  exfo  7077  f1ofveu  7381  zmax  12904  zbtwnre  12905  rebtwnz  12906  icoshftf1o  13435  divalgb  16374  1arith2  16899  ply1divalg2  26044  addsq2reu  27351  addsqn2reu  27352  addsqrexnreu  27353  2sqreultlem  27358  2sqreunnltlem  27361  frgr2wwlkeu  30256  numclwwlk2lem1  30305  numclwlk2lem2f1o  30308  pjhtheu2  31345  reuxfrdf  32420  xrsclat  32949  xrmulc1cn  33920  ply1divalg3  35629  poimirlem25  37639  hdmap14lem14  41875  cantnf2  43314  prproropreud  47510  quad1  47621  requad1  47623  requad2  47624  isuspgrim0lem  47893  isuspgrim0  47894  isuspgrimlem  47895  itscnhlinecirc02p  48774  reueqbidva  48794  reuxfr1dd  48795  uptrlem1  49199  isinito2lem  49487  lanup  49630  ranup  49631  islmd  49654  iscmd  49655