Theorem reubidva 3364

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

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

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  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539  df-eu 2569  df-reu 3351

This theorem is referenced by:  reubidv  3366  reuxfrd  3706  reuxfr1d  3708  fdmeu  6890  exfo  7050  f1ofveu  7352  zmax  12858  zbtwnre  12859  rebtwnz  12860  icoshftf1o  13390  divalgb  16331  1arith2  16856  ply1divalg2  26100  addsq2reu  27407  addsqn2reu  27408  addsqrexnreu  27409  2sqreultlem  27414  2sqreunnltlem  27417  frgr2wwlkeu  30402  numclwwlk2lem1  30451  numclwlk2lem2f1o  30454  pjhtheu2  31491  reuxfrdf  32565  xrsclat  33093  xrmulc1cn  34087  ply1divalg3  35836  poimirlem25  37846  hdmap14lem14  42141  cantnf2  43567  prproropreud  47755  quad1  47866  requad1  47868  requad2  47869  isuspgrim0lem  48139  isuspgrim0  48140  isuspgrimlem  48141  itscnhlinecirc02p  49031  reueqbidva  49051  reuxfr1dd  49052  uptrlem1  49455  isinito2lem  49743  lanup  49886  ranup  49887  islmd  49910  iscmd  49911