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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  reubidv  3363  reuxfrd  3703  reuxfr1d  3705  fdmeu  6887  exfo  7047  f1ofveu  7349  zmax  12849  zbtwnre  12850  rebtwnz  12851  icoshftf1o  13381  divalgb  16322  1arith2  16847  ply1divalg2  26091  addsq2reu  27398  addsqn2reu  27399  addsqrexnreu  27400  2sqreultlem  27405  2sqreunnltlem  27408  frgr2wwlkeu  30328  numclwwlk2lem1  30377  numclwlk2lem2f1o  30380  pjhtheu2  31417  reuxfrdf  32491  xrsclat  33021  xrmulc1cn  34015  ply1divalg3  35758  poimirlem25  37758  hdmap14lem14  42053  cantnf2  43482  prproropreud  47671  quad1  47782  requad1  47784  requad2  47785  isuspgrim0lem  48055  isuspgrim0  48056  isuspgrimlem  48057  itscnhlinecirc02p  48947  reueqbidva  48967  reuxfr1dd  48968  uptrlem1  49371  isinito2lem  49659  lanup  49802  ranup  49803  islmd  49826  iscmd  49827