Theorem abbidv 2795

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721

This theorem is referenced by:  rabbidva2  3407  cdeqab  3741  sbceqbid  3760  csbeq1  3865  csbeq2  3867  csbeq2d  3868  csbeq2dv  3869  csbprc  4372  sbcel12  4374  sbceqg  4375  csbnestgfw  4385  csbnestgf  4390  pweqALT  4578  sneq  4599  rabsneq  4608  csbsng  4672  uniprg  4887  csbuni  4900  inteq  4913  iineq1  4973  iineq2  4976  iuneq12d  4985  dfiin2g  4996  iinrab  5033  iinxprg  5053  opabbid  5172  opabbidv  5173  axrep6g  5245  imasng  6055  predres  6312  iotaeq  6476  iotabi  6477  dfimafn  6923  fliftf  7290  oprabbid  7454  oprabbidv  7455  frecseq123  8261  csbfrecsg  8263  rdglim2  8400  qseq1  8730  qseq2  8731  qsinxp  8766  mapvalg  8809  fsetexb  8837  ixpsnval  8873  ixpeq1  8881  fival  9363  tcvalg  9691  karden  9848  acneq  9996  infmap2  10170  cfval  10200  cflim3  10215  axdclem  10472  axdc  10474  rankcf  10730  genpv  10952  negfi  12132  supadd  12151  hashf1lem2  14421  hashf1  14422  hashfac  14423  csbwrdg  14509  cshimadifsn  14795  cshimadifsn0  14796  cleq1  14949  dfrtrcl2  15028  shftlem  15034  shftfib  15038  vdwlem6  16957  cshwsiun  17070  lubfval  18309  glbfval  18322  eqglact  19111  qus0subgbas  19130  isghm  19147  isghmOLD  19148  symgval  19301  sylow1lem2  19529  sylow3lem1  19557  efgval  19647  dmdprd  19930  ixpsnbasval  21115  pzriprnglem10  21400  pzriprnglem11  21401  cssval  21591  aspval2  21807  ressmplbas2  21934  tgval  22842  clsval2  22937  lpfval  23025  lpval  23026  islocfin  23404  ptval  23457  hauspwpwf1  23874  ptcmplem2  23940  snclseqg  24003  ustval  24090  itg2val  25629  limcfval  25773  plyval  26098  addsval  27869  addscom  27873  addsass  27912  addsbday  27924  mulsval  28012  mulscom  28042  addsdi  28058  mulsass  28069  mulsunif2lem  28072  precsexlemcbv  28108  precsexlem3  28111  halfcut  28333  elreno  28346  readdscl  28350  remulscl  28353  isismt  28461  nb3grprlem1  29307  vtxdun  29409  rgrx0ndm  29521  ewlksfval  29529  rusgrnumwwlkb0  29901  eclclwwlkn1  30004  avril1  30392  nmoofval  30691  nmooval  30692  nmoo0  30720  nmopval  31785  nmfnval  31805  iunrdx  32492  iinabrex  32498  disjabrex  32511  disjabrexf  32512  dfimafnf  32560  curry2ima  32632  cshwrnid  32883  nsgqusf1olem2  33385  pstmval  33885  pstmfval  33886  sigaval  34101  measval  34188  orvcval  34449  bnj956  34766  bnj18eq1  34917  bnj1318  35015  fnrelpredd  35079  derangval  35154  satfdm  35356  fmlasuc  35373  satffunlem1lem2  35390  satffunlem2lem2  35393  mclsval  35550  dfrdg2  35783  dfrdg3  35784  altxpeq1  35961  altxpeq2  35962  ixpeq12dv  36204  cbvcsbdavw  36247  cbvcsbdavw2  36248  cbviundavw  36250  cbviindavw  36251  cbvopab1davw  36252  cbvopab2davw  36253  cbvopabdavw  36254  cbviotadavw  36257  cbvoprab1davw  36259  cbvoprab2davw  36260  cbvoprab3davw  36261  cbvoprab123davw  36262  cbvoprab12davw  36263  cbvoprab23davw  36264  cbvoprab13davw  36265  cbvixpdavw  36266  cbviundavw2  36274  cbviindavw2  36275  cbvixpdavw2  36282  bj-snsetex  36951  bj-sngleq  36955  bj-projeq  36980  bj-projval  36984  bj-imafv  37239  csboprabg  37318  finxpeq1  37374  finxpeq2  37375  csbfinxpg  37376  finxpreclem6  37384  ptrest  37613  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  mblfinlem3  37653  cnambfre  37662  itg2addnc  37668  areacirclem5  37706  sdclem2  37736  sdc  37738  ismtyval  37794  elghomlem1OLD  37879  iineq12f  38158  eccnvepres  38268  lfl1dim  39114  ldual1dim  39159  glbconxN  39372  lineset  39732  pointsetN  39735  psubspset  39738  pmapglb2xN  39766  polval2N  39900  psubclsetN  39930  lautset  40076  pautsetN  40092  tendofset  40752  tendoset  40753  dva1dim  40979  dia1dim2  41056  dib1dim2  41162  diclspsn  41188  dih1dimatlem  41323  dihglb2  41336  hdmap1ffval  41789  hdmapffval  41820  hgmapffval  41879  sticksstones22  42156  sticksstones23  42157  aks6d1c6isolem3  42164  prjspeclsp  42600  sn-isghm  42661  eldiophb  42745  eldioph  42746  diophrw  42747  eldioph2  42750  eldioph2b  42751  eldioph3  42754  diophin  42760  diophun  42761  diophrex  42763  rexrabdioph  42782  rmxypairf1o  42900  hbtlem1  43112  hbtlem7  43114  tfsconcatrn  43331  nzss  44306  dropab1  44436  dropab2  44437  iineq12dv  45100  supsubc  45349  dfaimafn  47163  dfatsnafv2  47250  rnfdmpr  47279  f1oresf1o  47288  imasetpreimafvbijlemfo  47403  fargshiftfo  47440  sprval  47477  sprvalpw  47478  prprval  47512  prprvalpw  47513  prprspr2  47516  isgrim  47879  isgrlim  47978  setrecseq  49671