Theorem reubidva 3380

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

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

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 2565  df-eu 2595  df-reu 3367

This theorem is used by:  reubidv  3382  reuxfrd  3706  reuxfr1d  3708  fdmeu  6939  exfo  7103  f1ofveu  7412  zmax  13065  zbtwnre  13066  rebtwnz  13067  icoshftf1o  13598  divalgb  16567  1arith2  17099  ply1divalg2  26450  addsq2reu  27760  addsqn2reu  27761  addsqrexnreu  27762  2sqreultlem  27767  2sqreunnltlem  27770  angmgmaddeu1  29372  angmgmaddeu2  29373  angmgmaddeu3  29374  angmgmaddeu4  29375  angmgmaddeu5  29376  angmgmaddeu6  29377  angmgmaddeu7  29378  angmgmaddov2lem  29380  frgr2wwlkeu  30921  numclwwlk2lem1  30970  numclwlk2lem2f1o  30973  pjhtheu2  32011  reuxfrdf  33080  xrsclat  33565  xrmulc1cn  34555  ply1divalg3  36386  poimirlem25  38543  hdmap14lem14  42918  cantnf2  44311  prproropreud  48560  quad1  48687  requad1  48689  requad2  48690  isuspgrim0lem  48960  isuspgrim0  48961  isuspgrimlem  48962  itscnhlinecirc02p  49866  reueqbidva  49885  reuxfr1dd  49886  uptrlem1  50287  isinito2lem  50575  lanup  50718  ranup  50719  islmd  50742  iscmd  50743