Theorem reubidva 3380

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  ∃!weu 2594  ∃!wreu 3364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-mo 2565  df-eu 2595  df-reu 3367

This theorem is referenced by:  reubidv  3382  reuxfrd  3709  reuxfr1d  3711  fdmeu  6918  exfo  7081  f1ofveu  7385  zmax  12940  zbtwnre  12941  rebtwnz  12942  icoshftf1o  13472  divalgb  16429  1arith2  16955  ply1divalg2  26187  addsq2reu  27492  addsqn2reu  27493  addsqrexnreu  27494  2sqreultlem  27499  2sqreunnltlem  27502  frgr2wwlkeu  30486  numclwwlk2lem1  30535  numclwlk2lem2f1o  30538  pjhtheu2  31576  reuxfrdf  32649  xrsclat  33150  xrmulc1cn  34188  ply1divalg3  35953  poimirlem25  38105  hdmap14lem14  42466  cantnf2  43863  prproropreud  48076  quad1  48203  requad1  48205  requad2  48206  isuspgrim0lem  48476  isuspgrim0  48477  isuspgrimlem  48478  itscnhlinecirc02p  49368  reueqbidva  49388  reuxfr1dd  49389  uptrlem1  49792  isinito2lem  50080  lanup  50223  ranup  50224  islmd  50247  iscmd  50248