Theorem abbidv 2831

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561   = wceq 1563  {cab 2743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757

This theorem is referenced by:  rabbidva2  3419  cdeqab  3736  sbceqbid  3754  csbeq1  3858  csbeq2  3860  csbeq2d  3861  csbeq2dv  3862  csbprc  4366  sbcel12  4368  sbceqg  4369  csbnestgfw  4379  csbnestgf  4384  pweqALT  4573  sneq  4595  csbsng  4670  uniprg  4884  csbuni  4899  inteq  4911  iineq1  4970  iineq2  4973  iuneq12d  4982  dfiin2g  4991  iinrab  5029  iinxprg  5051  opabbid  5170  opabbidv  5171  axrep6g  5245  imasng  6077  predres  6330  iotaeq  6493  iotabi  6494  dfimafn  6933  fliftf  7303  oprabbid  7465  oprabbidv  7466  frecseq123  8267  csbfrecsg  8269  rdglim2  8407  qseq1  8742  qseq2  8743  snecg  8763  qsinxp  8779  mapvalg  8821  fsetexb  8849  ixpsnval  8886  ixpeq1  8894  fival  9360  tcvalg  9693  karden  9869  acneq  10015  infmap2  10188  cfval  10218  cflim3  10234  axdclem  10491  axdc  10493  rankcf  10750  genpv  10972  negfi  12155  supadd  12174  hashf1lem2  14483  hashf1  14484  hashfac  14485  csbwrdg  14571  cshimadifsn  14856  cshimadifsn0  14857  cleq1  15010  dfrtrcl2  15089  shftlem  15095  shftfib  15099  vdwlem6  17036  cshwsiun  17149  lubfval  18394  glbfval  18407  eqglact  19238  qus0subgbas  19260  isghm  19277  symgval  19432  sylow1lem2  19660  sylow3lem1  19688  efgval  19778  dmdprd  20061  ixpsnbasval  21298  pzriprnglem10  21600  pzriprnglem11  21601  cssval  21792  aspval2  22008  ressmplbas2  22137  tgval  23073  clsval2  23168  lpfval  23256  lpval  23257  islocfin  23635  ptval  23688  hauspwpwf1  24105  ptcmplem2  24171  snclseqg  24234  ustval  24321  itg2val  25848  limcfval  25992  plyval  26311  addsval  28113  addscom  28117  addsass  28156  addbday  28169  mulsval  28260  mulscom  28290  addsdi  28306  mulsass  28317  mulsunif2lem  28320  precsexlemcbv  28357  precsexlem3  28360  halfcut  28609  pw2cut2  28613  elreno  28642  readdscl  28650  remulscl  28653  isismt  28761  nb3grprlem1  29639  vtxdun  29740  rgrx0ndm  29852  ewlksfval  29860  rusgrnumwwlkb0  30232  eclclwwlkn1  30335  avril1  30723  nmoofval  31023  nmooval  31024  nmoo0  31052  nmopval  32117  nmfnval  32137  iunrdx  32818  iinabrex  32824  disjabrex  32837  disjabrexf  32838  dfimafnf  32893  curry2ima  32966  cshwrnid  33194  nsgqusf1olem2  33639  pstmval  34202  pstmfval  34203  sigaval  34418  measval  34505  orvcval  34765  bnj956  35082  bnj18eq1  35232  bnj1318  35330  fnrelpredd  35397  derangval  35530  satfdm  35732  fmlasuc  35749  satffunlem1lem2  35766  satffunlem2lem2  35769  mclsval  35926  dfrdg2  36156  dfrdg3  36157  altxpeq1  36336  altxpeq2  36337  ixpeq12dv  36589  cbvcsbdavw  36632  cbvcsbdavw2  36633  cbviundavw  36635  cbviindavw  36636  cbvopab1davw  36637  cbvopab2davw  36638  cbvopabdavw  36639  cbviotadavw  36642  cbvoprab1davw  36644  cbvoprab2davw  36645  cbvoprab3davw  36646  cbvoprab123davw  36647  cbvoprab12davw  36648  cbvoprab23davw  36649  cbvoprab13davw  36650  cbvixpdavw  36651  cbviundavw2  36659  cbviindavw2  36660  cbvixpdavw2  36667  bj-snsetex  37460  bj-sngleq  37464  bj-projeq  37489  bj-projval  37493  bj-imafv  37755  csboprabg  37836  finxpeq1  37892  finxpeq2  37893  csbfinxpg  37894  finxpreclem6  37902  ptrest  38130  poimirlem26  38157  poimirlem27  38158  poimirlem28  38159  mblfinlem3  38170  cnambfre  38179  itg2addnc  38185  areacirclem5  38223  sdclem2  38253  sdc  38255  ismtyval  38311  elghomlem1OLD  38396  iineq12f  38675  eccnvepres  38797  ecqmap  38960  lfl1dim  39757  ldual1dim  39802  glbconxN  40014  lineset  40374  pointsetN  40377  psubspset  40380  pmapglb2xN  40408  polval2N  40542  psubclsetN  40572  lautset  40718  pautsetN  40734  tendofset  41394  tendoset  41395  dva1dim  41621  dia1dim2  41698  dib1dim2  41804  diclspsn  41830  dih1dimatlem  41965  dihglb2  41978  hdmap1ffval  42431  hdmapffval  42462  hgmapffval  42521  sticksstones22  42797  sticksstones23  42798  aks6d1c6isolem3  42805  prjspeclsp  43206  sn-isghm  43267  eldiophb  43350  eldioph  43351  diophrw  43352  eldioph2  43355  eldioph2b  43356  eldioph3  43359  diophin  43365  diophun  43366  diophrex  43368  rexrabdioph  43383  rmxypairf1o  43500  hbtlem1  43712  hbtlem7  43714  tfsconcatrn  43931  nzss  44891  dropab1  45020  dropab2  45021  iineq12dv  45682  supsubc  45927  dfaimafn  47757  dfatsnafv2  47844  rnfdmpr  47873  f1oresf1o  47882  imasetpreimafvbijlemfo  48009  fargshiftfo  48046  sprval  48083  sprvalpw  48084  prprval  48118  prprvalpw  48119  prprspr2  48122  isgrim  48502  isgrlim  48602  setrecseq  50314