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

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
StepHypRef Expression
1 reubidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32reubidva 3102 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator