Theorem abbidv 2803

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542  {cab 2715

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 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729

This theorem is referenced by:  rabbidva2  3392  cdeqab  3717  sbceqbid  3736  csbeq1  3841  csbeq2  3843  csbeq2d  3844  csbeq2dv  3845  csbprc  4350  sbcel12  4352  sbceqg  4353  csbnestgfw  4363  csbnestgf  4368  pweqALT  4557  sneq  4578  csbsng  4653  uniprg  4867  csbuni  4881  inteq  4893  iineq1  4952  iineq2  4955  iuneq12d  4964  dfiin2g  4974  iinrab  5012  iinxprg  5032  opabbid  5151  opabbidv  5152  axrep6g  5225  imasng  6043  predres  6297  iotaeq  6460  iotabi  6461  dfimafn  6896  fliftf  7263  oprabbid  7425  oprabbidv  7426  frecseq123  8225  csbfrecsg  8227  rdglim2  8364  qseq1  8696  qseq2  8697  snecg  8717  qsinxp  8733  mapvalg  8776  fsetexb  8804  ixpsnval  8841  ixpeq1  8849  fival  9318  tcvalg  9648  karden  9810  acneq  9956  infmap2  10130  cfval  10160  cflim3  10175  axdclem  10432  axdc  10434  rankcf  10691  genpv  10913  negfi  12096  supadd  12115  hashf1lem2  14409  hashf1  14410  hashfac  14411  csbwrdg  14497  cshimadifsn  14782  cshimadifsn0  14783  cleq1  14936  dfrtrcl2  15015  shftlem  15021  shftfib  15025  vdwlem6  16948  cshwsiun  17061  lubfval  18305  glbfval  18318  eqglact  19145  qus0subgbas  19164  isghm  19181  isghmOLD  19182  symgval  19337  sylow1lem2  19565  sylow3lem1  19593  efgval  19683  dmdprd  19966  ixpsnbasval  21195  pzriprnglem10  21480  pzriprnglem11  21481  cssval  21672  aspval2  21888  ressmplbas2  22015  tgval  22930  clsval2  23025  lpfval  23113  lpval  23114  islocfin  23492  ptval  23545  hauspwpwf1  23962  ptcmplem2  24028  snclseqg  24091  ustval  24178  itg2val  25705  limcfval  25849  plyval  26168  addsval  27968  addscom  27972  addsass  28011  addbday  28024  mulsval  28115  mulscom  28145  addsdi  28161  mulsass  28172  mulsunif2lem  28175  precsexlemcbv  28212  precsexlem3  28215  halfcut  28464  pw2cut2  28468  elreno  28497  readdscl  28505  remulscl  28508  isismt  28616  nb3grprlem1  29463  vtxdun  29565  rgrx0ndm  29677  ewlksfval  29685  rusgrnumwwlkb0  30057  eclclwwlkn1  30160  avril1  30548  nmoofval  30848  nmooval  30849  nmoo0  30877  nmopval  31942  nmfnval  31962  iunrdx  32648  iinabrex  32654  disjabrex  32667  disjabrexf  32668  dfimafnf  32724  curry2ima  32797  cshwrnid  33036  nsgqusf1olem2  33489  pstmval  34055  pstmfval  34056  sigaval  34271  measval  34358  orvcval  34618  bnj956  34935  bnj18eq1  35085  bnj1318  35183  fnrelpredd  35250  derangval  35365  satfdm  35567  fmlasuc  35584  satffunlem1lem2  35601  satffunlem2lem2  35604  mclsval  35761  dfrdg2  35991  dfrdg3  35992  altxpeq1  36171  altxpeq2  36172  ixpeq12dv  36414  cbvcsbdavw  36457  cbvcsbdavw2  36458  cbviundavw  36460  cbviindavw  36461  cbvopab1davw  36462  cbvopab2davw  36463  cbvopabdavw  36464  cbviotadavw  36467  cbvoprab1davw  36469  cbvoprab2davw  36470  cbvoprab3davw  36471  cbvoprab123davw  36472  cbvoprab12davw  36473  cbvoprab23davw  36474  cbvoprab13davw  36475  cbvixpdavw  36476  cbviundavw2  36484  cbviindavw2  36485  cbvixpdavw2  36492  bj-snsetex  37286  bj-sngleq  37290  bj-projeq  37315  bj-projval  37319  bj-imafv  37581  csboprabg  37660  finxpeq1  37716  finxpeq2  37717  csbfinxpg  37718  finxpreclem6  37726  ptrest  37954  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  mblfinlem3  37994  cnambfre  38003  itg2addnc  38009  areacirclem5  38047  sdclem2  38077  sdc  38079  ismtyval  38135  elghomlem1OLD  38220  iineq12f  38499  eccnvepres  38621  ecqmap  38784  lfl1dim  39581  ldual1dim  39626  glbconxN  39838  lineset  40198  pointsetN  40201  psubspset  40204  pmapglb2xN  40232  polval2N  40366  psubclsetN  40396  lautset  40542  pautsetN  40558  tendofset  41218  tendoset  41219  dva1dim  41445  dia1dim2  41522  dib1dim2  41628  diclspsn  41654  dih1dimatlem  41789  dihglb2  41802  hdmap1ffval  42255  hdmapffval  42286  hgmapffval  42345  sticksstones22  42621  sticksstones23  42622  aks6d1c6isolem3  42629  prjspeclsp  43059  sn-isghm  43120  eldiophb  43203  eldioph  43204  diophrw  43205  eldioph2  43208  eldioph2b  43209  eldioph3  43212  diophin  43218  diophun  43219  diophrex  43221  rexrabdioph  43240  rmxypairf1o  43357  hbtlem1  43569  hbtlem7  43571  tfsconcatrn  43788  nzss  44762  dropab1  44891  dropab2  44892  iineq12dv  45554  supsubc  45801  dfaimafn  47625  dfatsnafv2  47712  rnfdmpr  47741  f1oresf1o  47750  imasetpreimafvbijlemfo  47877  fargshiftfo  47914  sprval  47951  sprvalpw  47952  prprval  47986  prprvalpw  47987  prprspr2  47990  isgrim  48370  isgrlim  48470  setrecseq  50172