Theorem reubidva 3379

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∃!weu 2593  ∃!wreu 3363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2564  df-eu 2594  df-reu 3366

This theorem is used by:  reubidv  3381  reuxfrd  3706  reuxfr1d  3708  fdmeu  6934  exfo  7098  f1ofveu  7407  zmax  12994  zbtwnre  12995  rebtwnz  12996  icoshftf1o  13527  divalgb  16494  1arith2  17020  ply1divalg2  26364  addsq2reu  27676  addsqn2reu  27677  addsqrexnreu  27678  2sqreultlem  27683  2sqreunnltlem  27686  angmgmaddeu1  29258  angmgmaddeu2  29259  angmgmaddeu3  29260  angmgmaddeu4  29261  angmgmaddeu5  29262  angmgmaddeu6  29263  angmgmaddeu7  29264  angmgmaddov2lem  29266  frgr2wwlkeu  30807  numclwwlk2lem1  30856  numclwlk2lem2f1o  30859  pjhtheu2  31897  reuxfrdf  32966  xrsclat  33451  xrmulc1cn  34440  ply1divalg3  36221  poimirlem25  38394  hdmap14lem14  42754  cantnf2  44166  prproropreud  48409  quad1  48536  requad1  48538  requad2  48539  isuspgrim0lem  48809  isuspgrim0  48810  isuspgrimlem  48811  itscnhlinecirc02p  49715  reueqbidva  49734  reuxfr1dd  49735  uptrlem1  50136  isinito2lem  50424  lanup  50567  ranup  50568  islmd  50591  iscmd  50592