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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  ∃!weu 2596  ∃!wreu 3367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597  df-reu 3370

This theorem is referenced by:  reubidv  3385  reuxfrd  3712  reuxfr1d  3714  fdmeu  6939  exfo  7102  f1ofveu  7406  zmax  12970  zbtwnre  12971  rebtwnz  12972  icoshftf1o  13502  divalgb  16463  1arith2  16989  ply1divalg2  26277  addsq2reu  27585  addsqn2reu  27586  addsqrexnreu  27587  2sqreultlem  27592  2sqreunnltlem  27595  frgr2wwlkeu  30659  numclwwlk2lem1  30708  numclwlk2lem2f1o  30711  pjhtheu2  31749  reuxfrdf  32818  xrsclat  33312  xrmulc1cn  34301  ply1divalg3  36115  poimirlem25  38277  hdmap14lem14  42636  cantnf2  44035  prproropreud  48241  quad1  48368  requad1  48370  requad2  48371  isuspgrim0lem  48641  isuspgrim0  48642  isuspgrimlem  48643  itscnhlinecirc02p  49548  reueqbidva  49567  reuxfr1dd  49568  uptrlem1  49971  isinito2lem  50259  lanup  50402  ranup  50403  islmd  50426  iscmd  50427