Theorem reubidva 3358

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  ∃!weu 2572  ∃!wreu 3342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-eu 2573  df-reu 3345

This theorem is referenced by:  reubidv  3360  reuxfrd  3689  reuxfr1d  3691  fdmeu  6883  exfo  7046  f1ofveu  7350  zmax  12886  zbtwnre  12887  rebtwnz  12888  icoshftf1o  13418  divalgb  16364  1arith2  16890  ply1divalg2  26122  addsq2reu  27421  addsqn2reu  27422  addsqrexnreu  27423  2sqreultlem  27428  2sqreunnltlem  27431  frgr2wwlkeu  30415  numclwwlk2lem1  30464  numclwlk2lem2f1o  30467  pjhtheu2  31505  reuxfrdf  32578  xrsclat  33090  xrmulc1cn  34114  ply1divalg3  35870  poimirlem25  38012  hdmap14lem14  42373  cantnf2  43770  prproropreud  47984  quad1  48111  requad1  48113  requad2  48114  isuspgrim0lem  48384  isuspgrim0  48385  isuspgrimlem  48386  itscnhlinecirc02p  49276  reueqbidva  49296  reuxfr1dd  49297  uptrlem1  49700  isinito2lem  49988  lanup  50131  ranup  50132  islmd  50155  iscmd  50156