Theorem reubidva 3366

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ∃!weu 2569  ∃!wreu 3350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-reu 3353

This theorem is referenced by:  reubidv  3368  reuxfrd  3708  reuxfr1d  3710  fdmeu  6898  exfo  7059  f1ofveu  7362  zmax  12870  zbtwnre  12871  rebtwnz  12872  icoshftf1o  13402  divalgb  16343  1arith2  16868  ply1divalg2  26112  addsq2reu  27419  addsqn2reu  27420  addsqrexnreu  27421  2sqreultlem  27426  2sqreunnltlem  27429  frgr2wwlkeu  30414  numclwwlk2lem1  30463  numclwlk2lem2f1o  30466  pjhtheu2  31503  reuxfrdf  32576  xrsclat  33103  xrmulc1cn  34107  ply1divalg3  35855  poimirlem25  37893  hdmap14lem14  42254  cantnf2  43679  prproropreud  47866  quad1  47977  requad1  47979  requad2  47980  isuspgrim0lem  48250  isuspgrim0  48251  isuspgrimlem  48252  itscnhlinecirc02p  49142  reueqbidva  49162  reuxfr1dd  49163  uptrlem1  49566  isinito2lem  49854  lanup  49997  ranup  49998  islmd  50021  iscmd  50022