Theorem abbidv 2808

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2173, 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 1931	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		abbi1 2807	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	2, 3	syl 17	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730

This theorem is referenced by:  rabbidva2  3400  cdeqab  3700  sbceqbid  3718  csbeq1  3831  csbeq2  3833  csbeq2d  3834  csbprc  4337  sbcel12  4339  sbceqg  4340  csbnestgfw  4350  csbnestgf  4355  pweqALT  4547  sneq  4568  csbsng  4641  unieqOLD  4848  uniprg  4853  csbuni  4867  inteq  4879  iineq1  4938  iineq2  4941  dfiin2g  4958  iinrab  4994  iinxprg  5014  opabbid  5135  opabbidv  5136  imasng  5980  iotaeq  6389  iotabi  6390  dfimafn  6814  fnsnfvOLD  6830  fliftf  7166  oprabbid  7318  oprabbidv  7319  frecseq123  8069  csbfrecsg  8071  wrecseq123OLD  8102  rdglim2  8234  qseq1  8510  qseq2  8511  qsinxp  8540  mapvalg  8583  fsetexb  8610  ixpsnval  8646  ixpeq1  8654  fival  9101  tcvalg  9427  karden  9584  acneq  9730  infmap2  9905  cfval  9934  cflim3  9949  axdclem  10206  axdc  10208  rankcf  10464  genpv  10686  negfi  11854  supadd  11873  hashf1lem2  14098  hashf1  14099  hashfac  14100  csbwrdg  14175  cshimadifsn  14470  cshimadifsn0  14471  cleq1  14622  dfrtrcl2  14701  shftlem  14707  shftfib  14711  vdwlem6  16615  cshwsiun  16729  lubfval  17983  glbfval  17996  eqglact  18722  isghm  18749  symgval  18891  sylow1lem2  19119  sylow3lem1  19147  efgval  19238  dmdprd  19516  ixpsnbasval  20393  cssval  20799  aspval2  21012  ressmplbas2  21138  tgval  22013  clsval2  22109  lpfval  22197  lpval  22198  islocfin  22576  ptval  22629  hauspwpwf1  23046  ptcmplem2  23112  snclseqg  23175  ustval  23262  itg2val  24798  limcfval  24941  plyval  25259  isismt  26799  nb3grprlem1  27650  vtxdun  27751  rgrx0ndm  27863  ewlksfval  27871  rusgrnumwwlkb0  28237  eclclwwlkn1  28340  avril1  28728  nmoofval  29025  nmooval  29026  nmoo0  29054  nmopval  30119  nmfnval  30139  iunrdx  30804  iinabrex  30809  disjabrex  30822  disjabrexf  30823  dfimafnf  30872  curry2ima  30943  cshwrnid  31135  nsgqusf1olem2  31501  pstmval  31747  pstmfval  31748  sigaval  31979  measval  32066  orvcval  32324  bnj956  32656  bnj18eq1  32807  bnj1318  32905  fnrelpredd  32961  derangval  33029  satfdm  33231  fmlasuc  33248  satffunlem1lem2  33265  satffunlem2lem2  33268  mclsval  33425  dfrdg2  33677  dfrdg3  33678  addsval  34053  addscom  34056  altxpeq1  34202  altxpeq2  34203  bj-snsetex  35080  bj-sngleq  35084  bj-projeq  35109  bj-projval  35113  bj-imafv  35349  csboprabg  35428  finxpeq1  35484  finxpeq2  35485  csbfinxpg  35486  finxpreclem6  35494  ptrest  35703  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  mblfinlem3  35743  cnambfre  35752  itg2addnc  35758  areacirclem5  35796  sdclem2  35827  sdc  35829  ismtyval  35885  elghomlem1OLD  35970  iineq12f  36249  eccnvepres  36342  lfl1dim  37062  ldual1dim  37107  glbconxN  37319  lineset  37679  pointsetN  37682  psubspset  37685  pmapglb2xN  37713  polval2N  37847  psubclsetN  37877  lautset  38023  pautsetN  38039  tendofset  38699  tendoset  38700  dva1dim  38926  dia1dim2  39003  dib1dim2  39109  diclspsn  39135  dih1dimatlem  39270  dihglb2  39283  hdmap1ffval  39736  hdmapffval  39767  hgmapffval  39826  sticksstones22  40052  prjspeclsp  40372  eldiophb  40495  eldioph  40496  diophrw  40497  eldioph2  40500  eldioph2b  40501  eldioph3  40504  diophin  40510  diophun  40511  diophrex  40513  rexrabdioph  40532  rmxypairf1o  40649  hbtlem1  40864  hbtlem7  40866  nzss  41824  dropab1  41954  dropab2  41955  supsubc  42782  dfaimafn  44544  dfatsnafv2  44631  rnfdmpr  44660  f1oresf1o  44669  imasetpreimafvbijlemfo  44745  fargshiftfo  44782  sprval  44819  sprvalpw  44820  prprval  44854  prprvalpw  44855  prprspr2  44858  setrecseq  46277