Theorem reubidva 3372

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∃!weu 2562  ∃!wreu 3354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2534  df-eu 2563  df-reu 3357

This theorem is referenced by:  reubidv  3374  reuxfrd  3722  reuxfr1d  3724  fdmeu  6920  exfo  7080  f1ofveu  7384  zmax  12911  zbtwnre  12912  rebtwnz  12913  icoshftf1o  13442  divalgb  16381  1arith2  16906  ply1divalg2  26051  addsq2reu  27358  addsqn2reu  27359  addsqrexnreu  27360  2sqreultlem  27365  2sqreunnltlem  27368  frgr2wwlkeu  30263  numclwwlk2lem1  30312  numclwlk2lem2f1o  30315  pjhtheu2  31352  reuxfrdf  32427  xrsclat  32956  xrmulc1cn  33927  ply1divalg3  35636  poimirlem25  37646  hdmap14lem14  41882  cantnf2  43321  prproropreud  47514  quad1  47625  requad1  47627  requad2  47628  isuspgrim0lem  47897  isuspgrim0  47898  isuspgrimlem  47899  itscnhlinecirc02p  48778  reueqbidva  48798  reuxfr1dd  48799  uptrlem1  49203  isinito2lem  49491  lanup  49634  ranup  49635  islmd  49658  iscmd  49659