Theorem abbidv 2802

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 2801	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	2, 3	syl 17	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

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

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 2708

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

This theorem is referenced by:  rabbidva2  3391  cdeqab  3716  sbceqbid  3735  csbeq1  3840  csbeq2  3842  csbeq2d  3843  csbeq2dv  3844  csbprc  4349  sbcel12  4351  sbceqg  4352  csbnestgfw  4362  csbnestgf  4367  pweqALT  4556  sneq  4577  csbsng  4652  uniprg  4866  csbuni  4880  inteq  4892  iineq1  4951  iineq2  4954  iuneq12d  4963  dfiin2g  4973  iinrab  5011  iinxprg  5031  opabbid  5150  opabbidv  5151  axrep6g  5225  imasng  6049  predres  6303  iotaeq  6466  iotabi  6467  dfimafn  6902  fliftf  7270  oprabbid  7432  oprabbidv  7433  frecseq123  8232  csbfrecsg  8234  rdglim2  8371  qseq1  8703  qseq2  8704  snecg  8724  qsinxp  8740  mapvalg  8783  fsetexb  8811  ixpsnval  8848  ixpeq1  8856  fival  9325  tcvalg  9657  karden  9819  acneq  9965  infmap2  10139  cfval  10169  cflim3  10184  axdclem  10441  axdc  10443  rankcf  10700  genpv  10922  negfi  12105  supadd  12124  hashf1lem2  14418  hashf1  14419  hashfac  14420  csbwrdg  14506  cshimadifsn  14791  cshimadifsn0  14792  cleq1  14945  dfrtrcl2  15024  shftlem  15030  shftfib  15034  vdwlem6  16957  cshwsiun  17070  lubfval  18314  glbfval  18327  eqglact  19154  qus0subgbas  19173  isghm  19190  isghmOLD  19191  symgval  19346  sylow1lem2  19574  sylow3lem1  19602  efgval  19692  dmdprd  19975  ixpsnbasval  21203  pzriprnglem10  21470  pzriprnglem11  21471  cssval  21662  aspval2  21878  ressmplbas2  22005  tgval  22920  clsval2  23015  lpfval  23103  lpval  23104  islocfin  23482  ptval  23535  hauspwpwf1  23952  ptcmplem2  24018  snclseqg  24081  ustval  24168  itg2val  25695  limcfval  25839  plyval  26158  addsval  27954  addscom  27958  addsass  27997  addbday  28010  mulsval  28101  mulscom  28131  addsdi  28147  mulsass  28158  mulsunif2lem  28161  precsexlemcbv  28198  precsexlem3  28201  halfcut  28450  pw2cut2  28454  elreno  28483  readdscl  28491  remulscl  28494  isismt  28602  nb3grprlem1  29449  vtxdun  29550  rgrx0ndm  29662  ewlksfval  29670  rusgrnumwwlkb0  30042  eclclwwlkn1  30145  avril1  30533  nmoofval  30833  nmooval  30834  nmoo0  30862  nmopval  31927  nmfnval  31947  iunrdx  32633  iinabrex  32639  disjabrex  32652  disjabrexf  32653  dfimafnf  32709  curry2ima  32782  cshwrnid  33021  nsgqusf1olem2  33474  pstmval  34039  pstmfval  34040  sigaval  34255  measval  34342  orvcval  34602  bnj956  34919  bnj18eq1  35069  bnj1318  35167  fnrelpredd  35234  derangval  35349  satfdm  35551  fmlasuc  35568  satffunlem1lem2  35585  satffunlem2lem2  35588  mclsval  35745  dfrdg2  35975  dfrdg3  35976  altxpeq1  36155  altxpeq2  36156  ixpeq12dv  36398  cbvcsbdavw  36441  cbvcsbdavw2  36442  cbviundavw  36444  cbviindavw  36445  cbvopab1davw  36446  cbvopab2davw  36447  cbvopabdavw  36448  cbviotadavw  36451  cbvoprab1davw  36453  cbvoprab2davw  36454  cbvoprab3davw  36455  cbvoprab123davw  36456  cbvoprab12davw  36457  cbvoprab23davw  36458  cbvoprab13davw  36459  cbvixpdavw  36460  cbviundavw2  36468  cbviindavw2  36469  cbvixpdavw2  36476  bj-snsetex  37270  bj-sngleq  37274  bj-projeq  37299  bj-projval  37303  bj-imafv  37565  csboprabg  37646  finxpeq1  37702  finxpeq2  37703  csbfinxpg  37704  finxpreclem6  37712  ptrest  37940  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  mblfinlem3  37980  cnambfre  37989  itg2addnc  37995  areacirclem5  38033  sdclem2  38063  sdc  38065  ismtyval  38121  elghomlem1OLD  38206  iineq12f  38485  eccnvepres  38607  ecqmap  38770  lfl1dim  39567  ldual1dim  39612  glbconxN  39824  lineset  40184  pointsetN  40187  psubspset  40190  pmapglb2xN  40218  polval2N  40352  psubclsetN  40382  lautset  40528  pautsetN  40544  tendofset  41204  tendoset  41205  dva1dim  41431  dia1dim2  41508  dib1dim2  41614  diclspsn  41640  dih1dimatlem  41775  dihglb2  41788  hdmap1ffval  42241  hdmapffval  42272  hgmapffval  42331  sticksstones22  42607  sticksstones23  42608  aks6d1c6isolem3  42615  prjspeclsp  43045  sn-isghm  43106  eldiophb  43189  eldioph  43190  diophrw  43191  eldioph2  43194  eldioph2b  43195  eldioph3  43198  diophin  43204  diophun  43205  diophrex  43207  rexrabdioph  43222  rmxypairf1o  43339  hbtlem1  43551  hbtlem7  43553  tfsconcatrn  43770  nzss  44744  dropab1  44873  dropab2  44874  iineq12dv  45536  supsubc  45783  dfaimafn  47613  dfatsnafv2  47700  rnfdmpr  47729  f1oresf1o  47738  imasetpreimafvbijlemfo  47865  fargshiftfo  47902  sprval  47939  sprvalpw  47940  prprval  47974  prprvalpw  47975  prprspr2  47978  isgrim  48358  isgrlim  48458  setrecseq  50160