Theorem reubidva 3356

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

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

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 2539  df-eu 2569  df-reu 3343

This theorem is referenced by:  reubidv  3358  reuxfrd  3694  reuxfr1d  3696  fdmeu  6896  exfo  7057  f1ofveu  7361  zmax  12895  zbtwnre  12896  rebtwnz  12897  icoshftf1o  13427  divalgb  16373  1arith2  16899  ply1divalg2  26104  addsq2reu  27403  addsqn2reu  27404  addsqrexnreu  27405  2sqreultlem  27410  2sqreunnltlem  27413  frgr2wwlkeu  30397  numclwwlk2lem1  30446  numclwlk2lem2f1o  30449  pjhtheu2  31487  reuxfrdf  32560  xrsclat  33071  xrmulc1cn  34074  ply1divalg3  35824  poimirlem25  37966  hdmap14lem14  42327  cantnf2  43753  prproropreud  47969  quad1  48096  requad1  48098  requad2  48099  isuspgrim0lem  48369  isuspgrim0  48370  isuspgrimlem  48371  itscnhlinecirc02p  49261  reueqbidva  49281  reuxfr1dd  49282  uptrlem1  49685  isinito2lem  49973  lanup  50116  ranup  50117  islmd  50140  iscmd  50141