Theorem reubidva 3357

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ∃!weu 2569  ∃!wreu 3341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-reu 3344

This theorem is referenced by:  reubidv  3359  reuxfrd  3695  reuxfr1d  3697  fdmeu  6890  exfo  7051  f1ofveu  7354  zmax  12886  zbtwnre  12887  rebtwnz  12888  icoshftf1o  13418  divalgb  16364  1arith2  16890  ply1divalg2  26114  addsq2reu  27417  addsqn2reu  27418  addsqrexnreu  27419  2sqreultlem  27424  2sqreunnltlem  27427  frgr2wwlkeu  30412  numclwwlk2lem1  30461  numclwlk2lem2f1o  30464  pjhtheu2  31502  reuxfrdf  32575  xrsclat  33086  xrmulc1cn  34090  ply1divalg3  35840  poimirlem25  37980  hdmap14lem14  42341  cantnf2  43771  prproropreud  47981  quad1  48108  requad1  48110  requad2  48111  isuspgrim0lem  48381  isuspgrim0  48382  isuspgrimlem  48383  itscnhlinecirc02p  49273  reueqbidva  49293  reuxfr1dd  49294  uptrlem1  49697  isinito2lem  49985  lanup  50128  ranup  50129  islmd  50152  iscmd  50153