Theorem reubidva 3375

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∃!weu 2567  ∃!wreu 3357

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 2539  df-eu 2568  df-reu 3360

This theorem is referenced by:  reubidv  3377  reuxfrd  3731  reuxfr1d  3733  fdmeu  6934  exfo  7094  f1ofveu  7397  zmax  12959  zbtwnre  12960  rebtwnz  12961  icoshftf1o  13489  divalgb  16421  1arith2  16946  ply1divalg2  26094  addsq2reu  27401  addsqn2reu  27402  addsqrexnreu  27403  2sqreultlem  27408  2sqreunnltlem  27411  frgr2wwlkeu  30254  numclwwlk2lem1  30303  numclwlk2lem2f1o  30306  pjhtheu2  31343  reuxfrdf  32418  xrsclat  32949  xrmulc1cn  33907  ply1divalg3  35610  poimirlem25  37615  hdmap14lem14  41846  cantnf2  43296  prproropreud  47471  quad1  47582  requad1  47584  requad2  47585  isuspgrim0lem  47854  isuspgrim0  47855  isuspgrimlem  47856  itscnhlinecirc02p  48713  reuxfr1dd  48733  isinito2lem  49331  lanup  49463  ranup  49464  islmd  49483  iscmd  49484