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 2144  ∃!weu 2593  ∃!wreu 3363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

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

This theorem is used by:  reubidv  3381  reuxfrd  3705  reuxfr1d  3707  fdmeu  6942  exfo  7106  f1ofveu  7415  zmax  13076  zbtwnre  13077  rebtwnz  13078  icoshftf1o  13609  divalgb  16580  1arith2  17112  ply1divalg2  26463  addsq2reu  27773  addsqn2reu  27774  addsqrexnreu  27775  2sqreultlem  27780  2sqreunnltlem  27783  angmgmaddeu1  29385  angmgmaddeu2  29386  angmgmaddeu3  29387  angmgmaddeu4  29388  angmgmaddeu5  29389  angmgmaddeu6  29390  angmgmaddeu7  29391  angmgmaddov2lem  29393  frgr2wwlkeu  30934  numclwwlk2lem1  30983  numclwlk2lem2f1o  30986  pjhtheu2  32024  reuxfrdf  33135  xrsclat  33619  xrmulc1cn  34609  ply1divalg3  36494  poimirlem25  38657  hdmap14lem14  43032  cantnf2  44421  prproropreud  48685  quad1  48812  requad1  48814  requad2  48815  isuspgrim0lem  49085  isuspgrim0  49086  isuspgrimlem  49087  itscnhlinecirc02p  49991  reueqbidva  50010  reuxfr1dd  50011  uptrlem1  50420  isinito2lem  50727  lanup  50918  ranup  50919  islmd  50942  iscmd  50943