Theorem abbidv 2800

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2171, 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

Step	Hyp	Ref	Expression
1		abbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alrimiv 1930	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		abbi 2799	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	2, 3	syl 17	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541  {cab 2708

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723

This theorem is referenced by:  rabbidva2  3407  cdeqab  3731  sbceqbid  3749  csbeq1  3861  csbeq2  3863  csbeq2d  3864  csbprc  4371  sbcel12  4373  sbceqg  4374  csbnestgfw  4384  csbnestgf  4389  pweqALT  4580  sneq  4601  csbsng  4674  unieqOLD  4882  uniprg  4887  csbuni  4902  inteq  4915  iineq1  4976  iineq2  4979  dfiin2g  4997  iinrab  5034  iinxprg  5054  opabbid  5175  opabbidv  5176  axrep6g  5255  imasng  6040  predres  6298  iotaeq  6466  iotabi  6467  dfimafn  6910  fnsnfvOLD  6926  fliftf  7265  oprabbid  7427  oprabbidv  7428  frecseq123  8218  csbfrecsg  8220  wrecseq123OLD  8251  rdglim2  8383  qseq1  8709  qseq2  8710  qsinxp  8739  mapvalg  8782  fsetexb  8809  ixpsnval  8845  ixpeq1  8853  fival  9357  tcvalg  9683  karden  9840  acneq  9988  infmap2  10163  cfval  10192  cflim3  10207  axdclem  10464  axdc  10466  rankcf  10722  genpv  10944  negfi  12113  supadd  12132  hashf1lem2  14367  hashf1  14368  hashfac  14369  csbwrdg  14444  cshimadifsn  14730  cshimadifsn0  14731  cleq1  14880  dfrtrcl2  14959  shftlem  14965  shftfib  14969  vdwlem6  16869  cshwsiun  16983  lubfval  18253  glbfval  18266  eqglact  18995  isghm  19022  symgval  19164  sylow1lem2  19395  sylow3lem1  19423  efgval  19513  dmdprd  19791  ixpsnbasval  20738  cssval  21123  aspval2  21338  ressmplbas2  21465  tgval  22342  clsval2  22438  lpfval  22526  lpval  22527  islocfin  22905  ptval  22958  hauspwpwf1  23375  ptcmplem2  23441  snclseqg  23504  ustval  23591  itg2val  25130  limcfval  25273  plyval  25591  addsval  27317  addscom  27321  addsass  27356  mulsval  27417  isismt  27539  nb3grprlem1  28391  vtxdun  28492  rgrx0ndm  28604  ewlksfval  28612  rusgrnumwwlkb0  28979  eclclwwlkn1  29082  avril1  29470  nmoofval  29767  nmooval  29768  nmoo0  29796  nmopval  30861  nmfnval  30881  iunrdx  31549  iinabrex  31554  disjabrex  31567  disjabrexf  31568  dfimafnf  31617  curry2ima  31690  cshwrnid  31885  nsgqusf1olem2  32266  pstmval  32565  pstmfval  32566  sigaval  32799  measval  32886  orvcval  33146  bnj956  33477  bnj18eq1  33628  bnj1318  33726  fnrelpredd  33782  derangval  33848  satfdm  34050  fmlasuc  34067  satffunlem1lem2  34084  satffunlem2lem2  34087  mclsval  34244  dfrdg2  34456  dfrdg3  34457  altxpeq1  34634  altxpeq2  34635  bj-snsetex  35507  bj-sngleq  35511  bj-projeq  35536  bj-projval  35540  bj-imafv  35795  csboprabg  35874  finxpeq1  35930  finxpeq2  35931  csbfinxpg  35932  finxpreclem6  35940  ptrest  36150  poimirlem26  36177  poimirlem27  36178  poimirlem28  36179  mblfinlem3  36190  cnambfre  36199  itg2addnc  36205  areacirclem5  36243  sdclem2  36274  sdc  36276  ismtyval  36332  elghomlem1OLD  36417  iineq12f  36696  eccnvepres  36813  lfl1dim  37656  ldual1dim  37701  glbconxN  37914  lineset  38274  pointsetN  38277  psubspset  38280  pmapglb2xN  38308  polval2N  38442  psubclsetN  38472  lautset  38618  pautsetN  38634  tendofset  39294  tendoset  39295  dva1dim  39521  dia1dim2  39598  dib1dim2  39704  diclspsn  39730  dih1dimatlem  39865  dihglb2  39878  hdmap1ffval  40331  hdmapffval  40362  hgmapffval  40421  sticksstones22  40649  prjspeclsp  41008  eldiophb  41138  eldioph  41139  diophrw  41140  eldioph2  41143  eldioph2b  41144  eldioph3  41147  diophin  41153  diophun  41154  diophrex  41156  rexrabdioph  41175  rmxypairf1o  41293  hbtlem1  41508  hbtlem7  41510  tfsconcatrn  41735  nzss  42719  dropab1  42849  dropab2  42850  supsubc  43708  dfaimafn  45517  dfatsnafv2  45604  rnfdmpr  45633  f1oresf1o  45642  imasetpreimafvbijlemfo  45717  fargshiftfo  45754  sprval  45791  sprvalpw  45792  prprval  45826  prprvalpw  45827  prprspr2  45830  setrecseq  47250