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

Theorem abbidv 2770
Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
Hypothesis
Ref Expression
abbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
abbidv (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1883 . 2 𝑥𝜑
2 abbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2abbid 2769 1 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  {cab 2637
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-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647
This theorem is referenced by:  rabbidva2  3217  cdeqab  3458  sbceqbid  3475  csbeq1  3569  csbeq2  3570  csbprc  4013  csbprcOLD  4014  sbcel12  4016  sbceqg  4017  csbeq2d  4024  csbnestgf  4029  pweq  4194  sneq  4220  csbsng  4275  rabsn  4288  unieq  4476  csbuni  4498  inteq  4510  iineq1  4567  iineq2  4570  dfiin2g  4585  iinrab  4614  iinxprg  4633  opabbid  4748  imasng  5522  iotaeq  5897  iotabi  5898  dfimafn  6284  fnsnfv  6297  fliftf  6605  oprabbid  6750  wrecseq123  7453  rdglim2  7573  qseq1  7839  qseq2  7840  qsinxp  7866  mapvalg  7909  ixpsnval  7953  ixpeq1  7961  fival  8359  tcvalg  8652  karden  8796  acneq  8904  infmap2  9078  cfval  9107  cflim3  9122  axdclem  9379  axdc  9381  rankcf  9637  genpv  9859  negfi  11009  supadd  11029  hashf1lem2  13278  hashf1  13279  hashfac  13280  csbwrdg  13366  cshimadifsn  13621  cshimadifsn0  13622  cleq1  13768  dfrtrcl2  13846  shftlem  13852  shftfib  13856  vdwlem6  15737  cshwsiun  15853  lubfval  17025  glbfval  17038  eqglact  17692  isghm  17707  symgval  17845  sylow1lem2  18060  sylow3lem1  18088  efgval  18176  dmdprd  18443  ixpsnbasval  19257  aspval2  19395  ressmplbas2  19503  cssval  20074  tgval  20807  clsval2  20902  lpfval  20990  lpval  20991  islocfin  21368  ptval  21421  hauspwpwf1  21838  ptcmplem2  21904  snclseqg  21966  ustval  22053  itg2val  23540  limcfval  23681  plyval  23994  isismt  25474  nb3grprlem1  26326  vtxdun  26433  rgrx0ndm  26545  ewlksfval  26553  wwlksnfi  26869  rusgrnumwwlkb0  26938  eclclwwlkn1  27039  avril1  27449  nmoofval  27745  nmooval  27746  nmoo0  27774  nmopval  28843  nmfnval  28863  iunrdx  29508  disjabrex  29521  disjabrexf  29522  dfimafnf  29564  curry2ima  29614  pstmval  30066  pstmfval  30067  sigaval  30301  measval  30389  orvcval  30647  bnj956  30973  bnj18eq1  31123  bnj1318  31219  derangval  31275  mclsval  31586  dfrdg2  31825  dfrdg3  31826  frecseq123  31902  altxpeq1  32205  altxpeq2  32206  bj-snsetex  33076  bj-sngleq  33080  bj-projeq  33105  bj-projval  33109  csbwrecsg  33303  csboprabg  33306  finxpeq1  33353  finxpeq2  33354  csbfinxpg  33355  finxpreclem6  33363  ptrest  33538  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  mblfinlem3  33578  cnambfre  33588  itg2addnc  33594  areacirclem5  33634  sdclem2  33668  sdc  33670  ismtyval  33729  elghomlem1OLD  33814  iineq12f  34103  eccnvepres  34186  lfl1dim  34726  ldual1dim  34771  glbconxN  34982  lineset  35342  pointsetN  35345  psubspset  35348  pmapglb2xN  35376  polval2N  35510  psubclsetN  35540  lautset  35686  pautsetN  35702  tendofset  36363  tendoset  36364  dva1dim  36590  dia1dim2  36668  dib1dim2  36774  diclspsn  36800  dih1dimatlem  36935  dihglb2  36948  hdmap1ffval  37402  hdmapffval  37435  hgmapffval  37494  eldiophb  37637  eldioph  37638  diophrw  37639  eldioph2  37642  eldioph2b  37643  eldioph3  37646  diophin  37653  diophun  37654  diophrex  37656  rexrabdioph  37675  rmxypairf1o  37793  hbtlem1  38010  hbtlem7  38012  nzss  38833  dropab1  38968  dropab2  38969  sbcel12gOLD  39071  csbxpgOLD  39368  csbrngOLD  39371  supsubc  39882  dfaimafn  41566  rnfdmpr  41623  fargshiftfo  41703  sprval  42054  sprvalpw  42055  setrecseq  42757
  Copyright terms: Public domain W3C validator