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

Theorem abbidv 2890
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 1995 . 2 𝑥𝜑
2 abbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2abbid 2889 1 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  {cab 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767
This theorem is referenced by:  rabbidva2  3336  cdeqab  3577  sbceqbid  3594  csbeq1  3685  csbeq2  3686  csbprc  4124  csbprcOLD  4125  sbcel12  4127  sbceqg  4128  csbeq2d  4135  csbnestgf  4140  pweq  4300  sneq  4326  csbsng  4380  rabsn  4392  unieq  4582  csbuni  4602  inteq  4614  iineq1  4669  iineq2  4672  dfiin2g  4687  iinrab  4716  iinxprg  4735  opabbid  4849  imasng  5628  iotaeq  6002  iotabi  6003  dfimafn  6387  fnsnfv  6400  fliftf  6708  oprabbid  6855  wrecseq123  7560  rdglim2  7681  qseq1  7948  qseq2  7949  qsinxp  7975  mapvalg  8019  ixpsnval  8065  ixpeq1  8073  fival  8474  tcvalg  8778  karden  8922  acneq  9066  infmap2  9242  cfval  9271  cflim3  9286  axdclem  9543  axdc  9545  rankcf  9801  genpv  10023  negfi  11173  supadd  11193  hashf1lem2  13442  hashf1  13443  hashfac  13444  csbwrdg  13530  cshimadifsn  13784  cshimadifsn0  13785  cleq1  13932  dfrtrcl2  14010  shftlem  14016  shftfib  14020  vdwlem6  15897  cshwsiun  16013  lubfval  17186  glbfval  17199  eqglact  17853  isghm  17868  symgval  18006  sylow1lem2  18221  sylow3lem1  18249  efgval  18337  dmdprd  18605  ixpsnbasval  19424  aspval2  19562  ressmplbas2  19670  cssval  20243  tgval  20980  clsval2  21075  lpfval  21163  lpval  21164  islocfin  21541  ptval  21594  hauspwpwf1  22011  ptcmplem2  22077  snclseqg  22139  ustval  22226  itg2val  23715  limcfval  23856  plyval  24169  isismt  25650  nb3grprlem1  26505  vtxdun  26612  rgrx0ndm  26724  ewlksfval  26732  wwlksnfi  27050  rusgrnumwwlkb0  27120  eclclwwlkn1  27233  avril1  27661  nmoofval  27957  nmooval  27958  nmoo0  27986  nmopval  29055  nmfnval  29075  iunrdx  29720  disjabrex  29733  disjabrexf  29734  dfimafnf  29776  curry2ima  29826  pstmval  30278  pstmfval  30279  sigaval  30513  measval  30601  orvcval  30859  bnj956  31185  bnj18eq1  31335  bnj1318  31431  derangval  31487  mclsval  31798  dfrdg2  32037  dfrdg3  32038  frecseq123  32114  altxpeq1  32417  altxpeq2  32418  bj-snsetex  33282  bj-sngleq  33286  bj-projeq  33311  bj-projval  33315  csbwrecsg  33510  csboprabg  33513  finxpeq1  33560  finxpeq2  33561  csbfinxpg  33562  finxpreclem6  33570  ptrest  33741  poimirlem26  33768  poimirlem27  33769  poimirlem28  33770  mblfinlem3  33781  cnambfre  33790  itg2addnc  33796  areacirclem5  33836  sdclem2  33870  sdc  33872  ismtyval  33931  elghomlem1OLD  34016  iineq12f  34305  eccnvepres  34388  lfl1dim  34930  ldual1dim  34975  glbconxN  35186  lineset  35546  pointsetN  35549  psubspset  35552  pmapglb2xN  35580  polval2N  35714  psubclsetN  35744  lautset  35890  pautsetN  35906  tendofset  36567  tendoset  36568  dva1dim  36794  dia1dim2  36872  dib1dim2  36978  diclspsn  37004  dih1dimatlem  37139  dihglb2  37152  hdmap1ffval  37605  hdmapffval  37636  hgmapffval  37695  eldiophb  37846  eldioph  37847  diophrw  37848  eldioph2  37851  eldioph2b  37852  eldioph3  37855  diophin  37862  diophun  37863  diophrex  37865  rexrabdioph  37884  rmxypairf1o  38002  hbtlem1  38219  hbtlem7  38221  nzss  39042  dropab1  39176  dropab2  39177  sbcel12gOLD  39279  csbxpgOLD  39576  csbrngOLD  39579  supsubc  40085  dfaimafn  41765  rnfdmpr  41823  f1oresf1o  41832  f1oresf1o2  41833  fargshiftfo  41906  sprval  42257  sprvalpw  42258  setrecseq  42960
  Copyright terms: Public domain W3C validator