Theorem abbidv 2828

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  {cab 2740

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754

This theorem is used by:  rabbidva2  3416  cdeqab  3731  sbceqbid  3749  csbeq1  3853  csbeq2  3855  csbeq2d  3856  csbeq2dv  3857  csbprc  4370  sbcel12  4372  sbceqg  4373  csbnestgfw  4383  csbnestgf  4388  pweqALT  4575  sneq  4597  csbsng  4672  uniprg  4886  csbuni  4901  inteq  4913  iineq1  4972  iineq2  4975  iuneq12d  4984  dfiin2g  4993  iinrab  5031  iinxprg  5053  opabbid  5174  opabbidv  5175  axrep6g  5249  imasng  6084  predres  6341  iotaeq  6505  iotabi  6506  dfimafn  6944  fliftf  7320  oprabbid  7482  oprabbidv  7483  frecseq123  8285  csbfrecsg  8287  rdglim2  8425  qseq1  8760  qseq2  8761  snecg  8781  qsinxp  8797  mapvalg  8839  fsetexb  8869  ixpsnval  8911  ixpeq1  8919  fival  9386  tcvalg  9719  karden  9902  kardenOLD  9903  acneq  10050  infmap2  10223  cfval  10252  cflim3  10268  axdclem  10525  axdc  10527  rankcf  10790  genpv  11012  negfi  12192  supadd  12211  hashf1lem2  14525  hashf1  14526  hashfac  14527  csbwrdg  14613  cshimadifsn  14904  cshimadifsn0  14905  cleq1  15060  dfrtrcl2  15139  shftlem  15145  shftfib  15149  vdwlem6  17084  cshwsiun  17197  lubfval  18442  glbfval  18455  eqglact  19310  qus0subgbas  19332  isghm  19349  symgval  19504  sylow1lem2  19732  sylow3lem1  19760  efgval  19850  dmdprd  20133  ixpsnbasval  21398  pzriprnglem10  21709  pzriprnglem11  21710  cssval  21901  aspval2  22119  ressmplbas2  22248  tgval  23186  clsval2  23281  lpfval  23369  lpval  23370  islocfin  23749  ptval  23802  hauspwpwf1  24219  ptcmplem2  24285  snclseqg  24348  ustval  24435  itg2val  25962  limcfval  26106  plyval  26425  addsval  28235  addscom  28239  addsass  28278  addbday  28291  mulsval  28382  mulscom  28412  addsdi  28428  mulsass  28439  mulsunif2lem  28442  precsexlemcbv  28479  precsexlem3  28482  halfcut  28731  pw2cut2  28735  elreno  28764  readdscl  28772  remulscl  28775  isismt  28884  nb3grprlem1  29848  vtxdun  29949  rgrx0ndm  30061  ewlksfval  30069  rusgrnumwwlkb0  30450  eclclwwlkn1  30553  avril1  30951  nmoofval  31251  nmooval  31252  nmoo0  31280  nmopval  32345  nmfnval  32365  iunrdx  33045  iinabrex  33050  disjabrex  33063  disjabrexf  33064  dfimafnf  33117  curry2ima  33189  cshwrnid  33409  nsgqusf1olem2  33851  pstmval  34413  pstmfval  34414  sigaval  34629  measval  34717  orvcval  34977  bnj956  35294  bnj18eq1  35444  bnj1318  35542  fnrelpredd  35604  kardval  35686  kard0  35688  derangval  35754  satfdm  35956  fmlasuc  35973  satffunlem1lem2  35990  satffunlem2lem2  35993  mclsval  36150  dfrdg2  36380  dfrdg3  36381  altxpeq1  36561  altxpeq2  36562  ixpeq12dv  36844  cbvcsbdavw  36887  cbvcsbdavw2  36888  cbviundavw  36890  cbviindavw  36891  cbvopab1davw  36892  cbvopab2davw  36893  cbvopabdavw  36894  cbviotadavw  36897  cbvoprab1davw  36899  cbvoprab2davw  36900  cbvoprab3davw  36901  cbvoprab123davw  36902  cbvoprab12davw  36903  cbvoprab23davw  36904  cbvoprab13davw  36905  cbvixpdavw  36906  cbviundavw2  36914  cbviindavw2  36915  cbvixpdavw2  36922  bj-snsetex  37715  bj-sngleq  37719  bj-projeq  37744  bj-projval  37748  bj-imafv  38011  csboprabg  38092  finxpeq1  38148  finxpeq2  38149  csbfinxpg  38150  finxpreclem6  38158  ptrest  38376  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  mblfinlem3  38416  cnambfre  38425  itg2addnc  38431  areacirclem5  38469  sdclem2  38500  sdc  38502  ismtyval  38558  elghomlem1OLD  38643  iineq12f  38920  eccnvepres  39042  ecqmap  39205  lfl1dim  40002  ldual1dim  40047  glbconxN  40259  lineset  40619  pointsetN  40622  psubspset  40625  pmapglb2xN  40653  polval2N  40787  psubclsetN  40817  lautset  40963  pautsetN  40979  tendofset  41639  tendoset  41640  dva1dim  41866  dia1dim2  41943  dib1dim2  42049  diclspsn  42075  dih1dimatlem  42210  dihglb2  42223  hdmap1ffval  42676  hdmapffval  42707  hgmapffval  42766  sticksstones22  43042  sticksstones23  43043  aks6d1c6isolem3  43050  prjspeclsp  43466  sn-isghm  43527  eldiophb  43610  eldioph  43611  diophrw  43612  eldioph2  43615  eldioph2b  43616  eldioph3  43619  diophin  43625  diophun  43626  diophrex  43628  rexrabdioph  43643  rmxypairf1o  43760  hbtlem1  43972  hbtlem7  43974  tfsconcatrn  44191  nzss  45149  dropab1  45278  dropab2  45279  iineq12dv  45946  supsubc  46191  dfaimafn  48061  dfatsnafv2  48148  rnfdmpr  48177  f1oresf1o  48186  imasetpreimafvbijlemfo  48313  fargshiftfo  48350  sprval  48387  sprvalpw  48388  prprval  48422  prprvalpw  48423  prprspr2  48426  isgrim  48806  isgrlim  48906  setrecseq  50619