Theorem reubidva 3155

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 13-Nov-2004.)

Hypothesis

Ref	Expression
reubidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reubidva

Step	Hyp	Ref	Expression
1		nfv 1883	. 2 ⊢ Ⅎ𝑥𝜑
2		reubidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	reubida 3154	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∈ wcel 2030  ∃!wreu 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750  df-eu 2502  df-reu 2948

This theorem is referenced by:  reubidv  3156  reuxfr2d  4921  reuxfrd  4923  exfo  6417  f1ofveu  6685  zmax  11823  zbtwnre  11824  rebtwnz  11825  icoshftf1o  12333  divalgb  15174  1arith2  15679  ply1divalg2  23943  frgr2wwlkeu  27307  numclwwlk2lem1  27356  numclwlk2lem2f1o  27359  numclwwlk2lem1OLD  27363  numclwlk2lem2f1oOLD  27366  pjhtheu2  28403  reuxfr3d  29456  reuxfr4d  29457  xrsclat  29808  xrmulc1cn  30104  poimirlem25  33564  hdmap14lem14  37490