Theorem reubidva 3101

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

Syntax hints:   → wi 4   ↔ wb 194   ∧ wa 382   ∈ wcel 1976  ∃!wreu 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033

This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1700  df-eu 2461  df-reu 2902

This theorem is referenced by:  reubidv  3102  reuxfr2d  4811  reuxfrd  4813  exfo  6269  f1ofveu  6521  zmax  11619  zbtwnre  11620  rebtwnz  11621  icoshftf1o  12124  divalgb  14913  1arith2  15418  ply1divalg2  23646  frg2woteu  26375  numclwwlk2lem1  26422  numclwlk2lem2f1o  26425  pjhtheu2  27452  reuxfr3d  28506  reuxfr4d  28507  xrsclat  28804  xrmulc1cn  29097  poimirlem25  32387  hdmap14lem14  35974  frgr2wwlkeu  41473  av-numclwwlk2lem1  41513  av-numclwlk2lem2f1o  41516