Theorem reubidva 3360

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2111  ∃!weu 2563  ∃!wreu 3344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2535  df-eu 2564  df-reu 3347

This theorem is referenced by:  reubidv  3362  reuxfrd  3702  reuxfr1d  3704  fdmeu  6873  exfo  7033  f1ofveu  7335  zmax  12838  zbtwnre  12839  rebtwnz  12840  icoshftf1o  13369  divalgb  16310  1arith2  16835  ply1divalg2  26066  addsq2reu  27373  addsqn2reu  27374  addsqrexnreu  27375  2sqreultlem  27380  2sqreunnltlem  27383  frgr2wwlkeu  30299  numclwwlk2lem1  30348  numclwlk2lem2f1o  30351  pjhtheu2  31388  reuxfrdf  32462  xrsclat  32984  xrmulc1cn  33935  ply1divalg3  35678  poimirlem25  37685  hdmap14lem14  41920  cantnf2  43358  prproropreud  47540  quad1  47651  requad1  47653  requad2  47654  isuspgrim0lem  47924  isuspgrim0  47925  isuspgrimlem  47926  itscnhlinecirc02p  48817  reueqbidva  48837  reuxfr1dd  48838  uptrlem1  49242  isinito2lem  49530  lanup  49673  ranup  49674  islmd  49697  iscmd  49698