Theorem reubidva 3390

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  ∃!weu 2602  ∃!wreu 3374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573  df-eu 2603  df-reu 3377

This theorem is referenced by:  reubidv  3392  reuxfrd  3720  reuxfr1d  3722  fdmeu  6935  exfo  7098  f1ofveu  7402  zmax  12965  zbtwnre  12966  rebtwnz  12967  icoshftf1o  13497  divalgb  16458  1arith2  16984  ply1divalg2  26261  addsq2reu  27566  addsqn2reu  27567  addsqrexnreu  27568  2sqreultlem  27573  2sqreunnltlem  27576  frgr2wwlkeu  30615  numclwwlk2lem1  30664  numclwlk2lem2f1o  30667  pjhtheu2  31705  reuxfrdf  32774  xrsclat  33268  xrmulc1cn  34261  ply1divalg3  36029  poimirlem25  38179  hdmap14lem14  42540  cantnf2  43937  prproropreud  48140  quad1  48267  requad1  48269  requad2  48270  isuspgrim0lem  48540  isuspgrim0  48541  isuspgrimlem  48542  itscnhlinecirc02p  49443  reueqbidva  49462  reuxfr1dd  49463  uptrlem1  49866  isinito2lem  50154  lanup  50297  ranup  50298  islmd  50321  iscmd  50322