MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reubidv Structured version   Visualization version   GIF version

Theorem reubidv 3102
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
StepHypRef Expression
1 reubidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 479 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32reubidva 3101 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  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 2032
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:  reueqd  3124  sbcreu  3481  oawordeu  7499  xpf1o  7984  dfac2  8813  creur  10861  creui  10862  divalg  14910  divalg2  14912  lubfval  16747  lubeldm  16750  lubval  16753  glbfval  16760  glbeldm  16763  glbval  16766  joineu  16779  meeteu  16793  dfod2  17750  ustuqtop  21802  isfrgra  26283  frgraunss  26288  frgra1v  26291  frgra2v  26292  frgra3v  26295  3vfriswmgra  26298  n4cyclfrgra  26311  riesz4  28113  cnlnadjeu  28127  poimirlem25  32407  poimirlem26  32408  hdmap1eulem  35934  hdmap1eulemOLDN  35935  hdmap14lem6  35986  usgredg2vtxeuALT  40451  isfrgr  41432  frcond1  41440  frgr1v  41443  nfrgr2v  41444  frgr3v  41447  3vfriswmgr  41450  n4cyclfrgr  41463
  Copyright terms: Public domain W3C validator