Theorem reubidv 3103

Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 17-Oct-1996.)

Hypothesis

Ref	Expression
reubidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem reubidv

Step	Hyp	Ref	Expression
1		reubidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	reubidva 3102	1 ⊢ (𝜑 → (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∈ 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:  reueqd  3125  sbcreu  3482  oawordeu  7522  xpf1o  8007  dfac2  8836  creur  10891  creui  10892  divalg  14964  divalg2  14966  lubfval  16801  lubeldm  16804  lubval  16807  glbfval  16814  glbeldm  16817  glbval  16820  joineu  16833  meeteu  16847  dfod2  17804  ustuqtop  21860  isfrgra  26517  frgraunss  26522  frgra1v  26525  frgra2v  26526  frgra3v  26529  3vfriswmgra  26532  n4cyclfrgra  26545  riesz4  28307  cnlnadjeu  28321  poimirlem25  32604  poimirlem26  32605  hdmap1eulem  36131  hdmap1eulemOLDN  36132  hdmap14lem6  36183  usgredg2vtxeuALT  40449  isfrgr  41430  frcond1  41438  frgr1v  41441  nfrgr2v  41442  frgr3v  41445  3vfriswmgr  41448  n4cyclfrgr  41461