Theorem abbidv 2799

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725

This theorem is referenced by:  rabbidva2  3398  cdeqab  3725  sbceqbid  3744  csbeq1  3849  csbeq2  3851  csbeq2d  3852  csbeq2dv  3853  csbprc  4358  sbcel12  4360  sbceqg  4361  csbnestgfw  4371  csbnestgf  4376  pweqALT  4564  sneq  4585  rabsneq  4594  csbsng  4660  uniprg  4874  csbuni  4888  inteq  4900  iineq1  4959  iineq2  4962  iuneq12d  4971  dfiin2g  4981  iinrab  5019  iinxprg  5039  opabbid  5158  opabbidv  5159  axrep6g  5230  imasng  6037  predres  6291  iotaeq  6454  iotabi  6455  dfimafn  6890  fliftf  7255  oprabbid  7417  oprabbidv  7418  frecseq123  8218  csbfrecsg  8220  rdglim2  8357  qseq1  8687  qseq2  8688  qsinxp  8723  mapvalg  8766  fsetexb  8794  ixpsnval  8830  ixpeq1  8838  fival  9303  tcvalg  9633  karden  9795  acneq  9941  infmap2  10115  cfval  10145  cflim3  10160  axdclem  10417  axdc  10419  rankcf  10675  genpv  10897  negfi  12078  supadd  12097  hashf1lem2  14365  hashf1  14366  hashfac  14367  csbwrdg  14453  cshimadifsn  14738  cshimadifsn0  14739  cleq1  14892  dfrtrcl2  14971  shftlem  14977  shftfib  14981  vdwlem6  16900  cshwsiun  17013  lubfval  18256  glbfval  18269  eqglact  19093  qus0subgbas  19112  isghm  19129  isghmOLD  19130  symgval  19285  sylow1lem2  19513  sylow3lem1  19541  efgval  19631  dmdprd  19914  ixpsnbasval  21144  pzriprnglem10  21429  pzriprnglem11  21430  cssval  21621  aspval2  21837  ressmplbas2  21963  tgval  22871  clsval2  22966  lpfval  23054  lpval  23055  islocfin  23433  ptval  23486  hauspwpwf1  23903  ptcmplem2  23969  snclseqg  24032  ustval  24119  itg2val  25657  limcfval  25801  plyval  26126  addsval  27906  addscom  27910  addsass  27949  addsbday  27961  mulsval  28049  mulscom  28079  addsdi  28095  mulsass  28106  mulsunif2lem  28109  precsexlemcbv  28145  precsexlem3  28148  halfcut  28379  pw2cut2  28383  elreno  28398  readdscl  28402  remulscl  28405  isismt  28513  nb3grprlem1  29360  vtxdun  29462  rgrx0ndm  29574  ewlksfval  29582  rusgrnumwwlkb0  29954  eclclwwlkn1  30057  avril1  30445  nmoofval  30744  nmooval  30745  nmoo0  30773  nmopval  31838  nmfnval  31858  iunrdx  32545  iinabrex  32551  disjabrex  32564  disjabrexf  32565  dfimafnf  32620  curry2ima  32694  cshwrnid  32949  nsgqusf1olem2  33386  pstmval  33929  pstmfval  33930  sigaval  34145  measval  34232  orvcval  34492  bnj956  34809  bnj18eq1  34960  bnj1318  35058  fnrelpredd  35123  derangval  35232  satfdm  35434  fmlasuc  35451  satffunlem1lem2  35468  satffunlem2lem2  35471  mclsval  35628  dfrdg2  35858  dfrdg3  35859  altxpeq1  36038  altxpeq2  36039  ixpeq12dv  36281  cbvcsbdavw  36324  cbvcsbdavw2  36325  cbviundavw  36327  cbviindavw  36328  cbvopab1davw  36329  cbvopab2davw  36330  cbvopabdavw  36331  cbviotadavw  36334  cbvoprab1davw  36336  cbvoprab2davw  36337  cbvoprab3davw  36338  cbvoprab123davw  36339  cbvoprab12davw  36340  cbvoprab23davw  36341  cbvoprab13davw  36342  cbvixpdavw  36343  cbviundavw2  36351  cbviindavw2  36352  cbvixpdavw2  36359  bj-snsetex  37028  bj-sngleq  37032  bj-projeq  37057  bj-projval  37061  bj-imafv  37316  csboprabg  37395  finxpeq1  37451  finxpeq2  37452  csbfinxpg  37453  finxpreclem6  37461  ptrest  37679  poimirlem26  37706  poimirlem27  37707  poimirlem28  37708  mblfinlem3  37719  cnambfre  37728  itg2addnc  37734  areacirclem5  37772  sdclem2  37802  sdc  37804  ismtyval  37860  elghomlem1OLD  37945  iineq12f  38224  eccnvepres  38338  lfl1dim  39240  ldual1dim  39285  glbconxN  39497  lineset  39857  pointsetN  39860  psubspset  39863  pmapglb2xN  39891  polval2N  40025  psubclsetN  40055  lautset  40201  pautsetN  40217  tendofset  40877  tendoset  40878  dva1dim  41104  dia1dim2  41181  dib1dim2  41287  diclspsn  41313  dih1dimatlem  41448  dihglb2  41461  hdmap1ffval  41914  hdmapffval  41945  hgmapffval  42004  sticksstones22  42281  sticksstones23  42282  aks6d1c6isolem3  42289  prjspeclsp  42730  sn-isghm  42791  eldiophb  42874  eldioph  42875  diophrw  42876  eldioph2  42879  eldioph2b  42880  eldioph3  42883  diophin  42889  diophun  42890  diophrex  42892  rexrabdioph  42911  rmxypairf1o  43028  hbtlem1  43240  hbtlem7  43242  tfsconcatrn  43459  nzss  44434  dropab1  44563  dropab2  44564  iineq12dv  45227  supsubc  45476  dfaimafn  47289  dfatsnafv2  47376  rnfdmpr  47405  f1oresf1o  47414  imasetpreimafvbijlemfo  47529  fargshiftfo  47566  sprval  47603  sprvalpw  47604  prprval  47638  prprvalpw  47639  prprspr2  47642  isgrim  48006  isgrlim  48106  setrecseq  49810