Theorem reubidva 3292

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
reubidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
reubidva	⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidva

Step	Hyp	Ref	Expression
1		reubidva.1	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 582	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	eubidv 2588	. 2 ⊢ (𝜑 → (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)))
4		df-reu 3061	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
5		df-reu 3061	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜒 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2114  ∃!weu 2570  ∃!wreu 3056

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-mo 2541  df-eu 2571  df-reu 3061

This theorem is referenced by:  reubidv  3293  reuxfrd  3652  reuxfr1d  3654  exfo  6894  f1ofveu  7178  zmax  12440  zbtwnre  12441  rebtwnz  12442  icoshftf1o  12961  divalgb  15862  1arith2  16377  ply1divalg2  24904  addsq2reu  26189  addsqn2reu  26190  addsqrexnreu  26191  2sqreultlem  26196  2sqreunnltlem  26199  frgr2wwlkeu  28277  numclwwlk2lem1  28326  numclwlk2lem2f1o  28329  pjhtheu2  29364  reuxfrdf  30426  xrsclat  30879  xrmulc1cn  31465  poimirlem25  35458  hdmap14lem14  39551  prproropreud  44543  quad1  44654  requad1  44656  requad2  44657  itscnhlinecirc02p  45713