Theorem reubidva 3391

Description: Formula-building rule for restricted existential 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 578	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	eubidv 2579	. 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-reu 3376	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-reu 3376	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2105  ∃!weu 2561  ∃!wreu 3373

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 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-mo 2533  df-eu 2562  df-reu 3376

This theorem is referenced by:  reubidv  3393  reuxfrd  3744  reuxfr1d  3746  exfo  7106  f1ofveu  7406  zmax  12936  zbtwnre  12937  rebtwnz  12938  icoshftf1o  13458  divalgb  16354  1arith2  16868  ply1divalg2  25993  addsq2reu  27285  addsqn2reu  27286  addsqrexnreu  27287  2sqreultlem  27292  2sqreunnltlem  27295  frgr2wwlkeu  30012  numclwwlk2lem1  30061  numclwlk2lem2f1o  30064  pjhtheu2  31101  reuxfrdf  32163  xrsclat  32613  xrmulc1cn  33373  poimirlem25  36976  hdmap14lem14  41215  cantnf2  42537  prproropreud  46635  quad1  46746  requad1  46748  requad2  46749  itscnhlinecirc02p  47632