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

Theorem abbidv 2882
Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2167, 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 1919 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 abbi1 2881 . 2 (∀𝑥(𝜓𝜒) → {𝑥𝜓} = {𝑥𝜒})
42, 3syl 17 1 (𝜑 → {𝑥𝜓} = {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526   = wceq 1528  {cab 2796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811
This theorem is referenced by:  rabbidva2  3474  cdeqab  3758  sbceqbid  3776  csbeq1  3883  csbeq2  3885  csbeq2d  3886  csbprc  4355  sbcel12  4357  sbceqg  4358  csbnestgfw  4368  csbnestgf  4373  pweq  4538  sneq  4567  csbsng  4636  unieq  4838  csbuni  4858  inteq  4870  iineq1  4927  iineq2  4930  dfiin2g  4948  iinrab  4982  iinxprg  5002  opabbid  5122  imasng  5944  iotaeq  6319  iotabi  6320  dfimafn  6721  fnsnfv  6736  fliftf  7057  oprabbid  7208  wrecseq123  7937  rdglim2  8057  qseq1  8332  qseq2  8333  qsinxp  8362  mapvalg  8405  ixpsnval  8452  ixpeq1  8460  fival  8864  tcvalg  9168  karden  9312  acneq  9457  infmap2  9628  cfval  9657  cflim3  9672  axdclem  9929  axdc  9931  rankcf  10187  genpv  10409  negfi  11577  supadd  11597  hashf1lem2  13802  hashf1  13803  hashfac  13804  csbwrdg  13883  cshimadifsn  14179  cshimadifsn0  14180  cleq1  14331  dfrtrcl2  14409  shftlem  14415  shftfib  14419  vdwlem6  16310  cshwsiun  16421  lubfval  17576  glbfval  17589  eqglact  18269  isghm  18296  symgval  18435  sylow1lem2  18653  sylow3lem1  18681  efgval  18772  dmdprd  19049  ixpsnbasval  19910  aspval2  20055  ressmplbas2  20164  cssval  20754  tgval  21491  clsval2  21586  lpfval  21674  lpval  21675  islocfin  22053  ptval  22106  hauspwpwf1  22523  ptcmplem2  22589  snclseqg  22651  ustval  22738  itg2val  24256  limcfval  24397  plyval  24710  isismt  26247  nb3grprlem1  27089  vtxdun  27190  rgrx0ndm  27302  ewlksfval  27310  wwlksnfiOLD  27612  rusgrnumwwlkb0  27677  eclclwwlkn1  27781  avril1  28169  nmoofval  28466  nmooval  28467  nmoo0  28495  nmopval  29560  nmfnval  29580  iunrdx  30243  disjabrex  30260  disjabrexf  30261  dfimafnf  30309  curry2ima  30370  cshwrnid  30562  pstmval  31034  pstmfval  31035  sigaval  31269  measval  31356  orvcval  31614  bnj956  31947  bnj18eq1  32098  bnj1318  32194  derangval  32311  satfdm  32513  fmlasuc  32530  satffunlem1lem2  32547  satffunlem2lem2  32550  mclsval  32707  dfrdg2  32937  dfrdg3  32938  frecseq123  33016  altxpeq1  33331  altxpeq2  33332  bj-snsetex  34172  bj-sngleq  34176  bj-projeq  34201  bj-projval  34205  bj-imafv  34425  csbwrecsg  34490  csboprabg  34493  finxpeq1  34549  finxpeq2  34550  csbfinxpg  34551  finxpreclem6  34559  ptrest  34772  poimirlem26  34799  poimirlem27  34800  poimirlem28  34801  mblfinlem3  34812  cnambfre  34821  itg2addnc  34827  areacirclem5  34867  sdclem2  34898  sdc  34900  ismtyval  34959  elghomlem1OLD  35044  iineq12f  35323  eccnvepres  35418  lfl1dim  36137  ldual1dim  36182  glbconxN  36394  lineset  36754  pointsetN  36757  psubspset  36760  pmapglb2xN  36788  polval2N  36922  psubclsetN  36952  lautset  37098  pautsetN  37114  tendofset  37774  tendoset  37775  dva1dim  38001  dia1dim2  38078  dib1dim2  38184  diclspsn  38210  dih1dimatlem  38345  dihglb2  38358  hdmap1ffval  38811  hdmapffval  38842  hgmapffval  38901  prjspeclsp  39140  eldiophb  39232  eldioph  39233  diophrw  39234  eldioph2  39237  eldioph2b  39238  eldioph3  39241  diophin  39247  diophun  39248  diophrex  39250  rexrabdioph  39269  rmxypairf1o  39386  hbtlem1  39601  hbtlem7  39603  nzss  40526  dropab1  40656  dropab2  40657  supsubc  41497  dfaimafn  43241  dfatsnafv2  43328  rnfdmpr  43357  f1oresf1o  43366  imasetpreimafvbijlemfo  43442  fargshiftfo  43479  sprval  43518  sprvalpw  43519  prprval  43553  prprvalpw  43554  prprspr2  43557  setrecseq  44716
  Copyright terms: Public domain W3C validator