Theorem reubidva 3102

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 1830	. 2 ⊢ Ⅎ𝑥𝜑
2		reubidva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	1, 2	reubida 3101	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∃!wreu 2898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701  df-eu 2462  df-reu 2903

This theorem is referenced by:  reubidv  3103  reuxfr2d  4817  reuxfrd  4819  exfo  6285  f1ofveu  6544  zmax  11661  zbtwnre  11662  rebtwnz  11663  icoshftf1o  12166  divalgb  14965  1arith2  15470  ply1divalg2  23702  frg2woteu  26582  numclwwlk2lem1  26629  numclwlk2lem2f1o  26632  pjhtheu2  27659  reuxfr3d  28713  reuxfr4d  28714  xrsclat  29011  xrmulc1cn  29304  poimirlem25  32604  hdmap14lem14  36191  frgr2wwlkeu  41492  av-numclwwlk2lem1  41532  av-numclwlk2lem2f1o  41535