Theorem reubidva 3383

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  ∃!weu 2596  ∃!wreu 3367

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 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567  df-eu 2597  df-reu 3370

This theorem is used by:  reubidv  3385  reuxfrd  3709  reuxfr1d  3711  fdmeu  6972  exfo  7137  f1ofveu  7445  zmax  13112  zbtwnre  13113  rebtwnz  13114  icoshftf1o  13645  divalgb  16618  1arith2  17150  ply1divalg2  26512  addsq2reu  27824  addsqn2reu  27825  addsqrexnreu  27826  2sqreultlem  27831  2sqreunnltlem  27834  angmgmaddeu1  29436  angmgmaddeu2  29437  angmgmaddeu3  29438  angmgmaddeu4  29439  angmgmaddeu5  29440  angmgmaddeu6  29441  angmgmaddeu7  29442  angmgmaddov2lem  29444  frgr2wwlkeu  30985  numclwwlk2lem1  31034  numclwlk2lem2f1o  31037  pjhtheu2  32075  reuxfrdf  33186  xrsclat  33671  xrmulc1cn  34673  ply1divalg3  36615  poimirlem25  38831  hdmap14lem14  43204  cantnf2  44588  prproropreud  48864  quad1  48991  requad1  48993  requad2  48994  isuspgrim0lem  49264  isuspgrim0  49265  isuspgrimlem  49266  itscnhlinecirc02p  50228  reueqbidva  50247  reuxfr1dd  50248  uptrlem1  50657  isinito2lem  50964  lanup  51155  ranup  51156  islmd  51179  iscmd  51180