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

Theorem reubidv 3156
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 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32reubidva 3155 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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:  reueqd  3178  sbcreu  3548  oawordeu  7680  xpf1o  8163  dfac2  8991  creur  11052  creui  11053  divalg  15173  divalg2  15175  lubfval  17025  lubeldm  17028  lubval  17031  glbfval  17038  glbeldm  17041  glbval  17044  joineu  17057  meeteu  17071  dfod2  18027  ustuqtop  22097  usgredg2vtxeuALT  26159  isfrgr  27238  frcond1  27246  frgr1v  27251  nfrgr2v  27252  frgr3v  27255  3vfriswmgr  27258  n4cyclfrgr  27271  eulplig  27467  riesz4  29051  cnlnadjeu  29065  poimirlem25  33564  poimirlem26  33565  hdmap1eulem  37430  hdmap1eulemOLDN  37431  hdmap14lem6  37482
  Copyright terms: Public domain W3C validator