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

Theorem abbidv 2888
Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2179, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.)
Hypothesis
Ref Expression
abbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
abbidv (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv
StepHypRef Expression
1 abbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21alrimiv 1929 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 abbi1 2887 . 2 (∀𝑥(𝜓𝜒) → {𝑥𝜓} = {𝑥𝜒})
42, 3syl 17 1 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1536   = wceq 1538  {cab 2802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817
This theorem is referenced by:  rabbidva2  3462  cdeqab  3747  sbceqbid  3765  csbeq1  3869  csbeq2  3871  csbeq2d  3872  csbprc  4341  sbcel12  4343  sbceqg  4344  csbnestgfw  4354  csbnestgf  4359  pweqALT  4539  sneq  4560  csbsng  4629  opeq1  4788  opeq2  4790  unieqOLD  4837  csbuni  4854  inteq  4866  iineq1  4923  iineq2  4926  dfiin2g  4944  iinrab  4978  iinxprg  4998  opabbid  5118  imasng  5939  iotaeq  6315  iotabi  6316  dfimafn  6717  fnsnfv  6732  fliftf  7058  oprabbid  7209  wrecseq123  7940  rdglim2  8060  qseq1  8335  qseq2  8336  qsinxp  8365  mapvalg  8408  ixpsnval  8456  ixpeq1  8464  fival  8869  tcvalg  9173  karden  9317  acneq  9463  infmap2  9634  cfval  9663  cflim3  9678  axdclem  9935  axdc  9937  rankcf  10193  genpv  10415  negfi  11583  supadd  11603  hashf1lem2  13817  hashf1  13818  hashfac  13819  csbwrdg  13894  cshimadifsn  14189  cshimadifsn0  14190  cleq1  14341  dfrtrcl2  14419  shftlem  14425  shftfib  14429  vdwlem6  16318  cshwsiun  16431  lubfval  17586  glbfval  17599  eqglact  18329  isghm  18356  symgval  18495  sylow1lem2  18722  sylow3lem1  18750  efgval  18841  dmdprd  19118  ixpsnbasval  19977  aspval2  20122  ressmplbas2  20231  cssval  20821  tgval  21558  clsval2  21653  lpfval  21741  lpval  21742  islocfin  22120  ptval  22173  hauspwpwf1  22590  ptcmplem2  22656  snclseqg  22719  ustval  22806  itg2val  24330  limcfval  24473  plyval  24788  isismt  26326  nb3grprlem1  27168  vtxdun  27269  rgrx0ndm  27381  ewlksfval  27389  rusgrnumwwlkb0  27755  eclclwwlkn1  27858  avril1  28246  nmoofval  28543  nmooval  28544  nmoo0  28572  nmopval  29637  nmfnval  29657  iunrdx  30321  disjabrex  30338  disjabrexf  30339  dfimafnf  30387  curry2ima  30450  cshwrnid  30641  pstmval  31165  pstmfval  31166  sigaval  31397  measval  31484  orvcval  31742  bnj956  32075  bnj18eq1  32226  bnj1318  32324  derangval  32441  satfdm  32643  fmlasuc  32660  satffunlem1lem2  32677  satffunlem2lem2  32680  mclsval  32837  dfrdg2  33067  dfrdg3  33068  frecseq123  33146  altxpeq1  33461  altxpeq2  33462  bj-snsetex  34313  bj-sngleq  34317  bj-projeq  34342  bj-projval  34346  bj-imafv  34581  csbwrecsg  34658  csboprabg  34661  finxpeq1  34717  finxpeq2  34718  csbfinxpg  34719  finxpreclem6  34727  ptrest  34968  poimirlem26  34995  poimirlem27  34996  poimirlem28  34997  mblfinlem3  35008  cnambfre  35017  itg2addnc  35023  areacirclem5  35061  sdclem2  35092  sdc  35094  ismtyval  35150  elghomlem1OLD  35235  iineq12f  35514  eccnvepres  35609  lfl1dim  36329  ldual1dim  36374  glbconxN  36586  lineset  36946  pointsetN  36949  psubspset  36952  pmapglb2xN  36980  polval2N  37114  psubclsetN  37144  lautset  37290  pautsetN  37306  tendofset  37966  tendoset  37967  dva1dim  38193  dia1dim2  38270  dib1dim2  38376  diclspsn  38402  dih1dimatlem  38537  dihglb2  38550  hdmap1ffval  39003  hdmapffval  39034  hgmapffval  39093  prjspeclsp  39462  eldiophb  39554  eldioph  39555  diophrw  39556  eldioph2  39559  eldioph2b  39560  eldioph3  39563  diophin  39569  diophun  39570  diophrex  39572  rexrabdioph  39591  rmxypairf1o  39708  hbtlem1  39923  hbtlem7  39925  nzss  40881  dropab1  41011  dropab2  41012  supsubc  41851  dfaimafn  43587  dfatsnafv2  43674  rnfdmpr  43703  f1oresf1o  43712  imasetpreimafvbijlemfo  43788  fargshiftfo  43825  sprval  43862  sprvalpw  43863  prprval  43897  prprvalpw  43898  prprspr2  43901  setrecseq  45069
  Copyright terms: Public domain W3C validator