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  3398  cdeqab  3732  sbceqbid  3751  csbeq1  3856  csbeq2  3858  csbeq2d  3859  csbeq2dv  3860  csbprc  4362  sbcel12  4364  sbceqg  4365  csbnestgfw  4375  csbnestgf  4380  pweqALT  4568  sneq  4589  rabsneq  4598  csbsng  4662  uniprg  4877  csbuni  4890  inteq  4902  iineq1  4962  iineq2  4965  iuneq12d  4974  dfiin2g  4984  iinrab  5021  iinxprg  5041  opabbid  5160  opabbidv  5161  axrep6g  5232  imasng  6039  predres  6291  iotaeq  6454  iotabi  6455  dfimafn  6889  fliftf  7256  oprabbid  7418  oprabbidv  7419  frecseq123  8222  csbfrecsg  8224  rdglim2  8361  qseq1  8691  qseq2  8692  qsinxp  8727  mapvalg  8770  fsetexb  8798  ixpsnval  8834  ixpeq1  8842  fival  9321  tcvalg  9653  karden  9810  acneq  9956  infmap2  10130  cfval  10160  cflim3  10175  axdclem  10432  axdc  10434  rankcf  10690  genpv  10912  negfi  12092  supadd  12111  hashf1lem2  14381  hashf1  14382  hashfac  14383  csbwrdg  14469  cshimadifsn  14754  cshimadifsn0  14755  cleq1  14908  dfrtrcl2  14987  shftlem  14993  shftfib  14997  vdwlem6  16916  cshwsiun  17029  lubfval  18272  glbfval  18285  eqglact  19076  qus0subgbas  19095  isghm  19112  isghmOLD  19113  symgval  19268  sylow1lem2  19496  sylow3lem1  19524  efgval  19614  dmdprd  19897  ixpsnbasval  21130  pzriprnglem10  21415  pzriprnglem11  21416  cssval  21607  aspval2  21823  ressmplbas2  21950  tgval  22858  clsval2  22953  lpfval  23041  lpval  23042  islocfin  23420  ptval  23473  hauspwpwf1  23890  ptcmplem2  23956  snclseqg  24019  ustval  24106  itg2val  25645  limcfval  25789  plyval  26114  addsval  27892  addscom  27896  addsass  27935  addsbday  27947  mulsval  28035  mulscom  28065  addsdi  28081  mulsass  28092  mulsunif2lem  28095  precsexlemcbv  28131  precsexlem3  28134  halfcut  28364  elreno  28382  readdscl  28386  remulscl  28389  isismt  28497  nb3grprlem1  29343  vtxdun  29445  rgrx0ndm  29557  ewlksfval  29565  rusgrnumwwlkb0  29934  eclclwwlkn1  30037  avril1  30425  nmoofval  30724  nmooval  30725  nmoo0  30753  nmopval  31818  nmfnval  31838  iunrdx  32525  iinabrex  32531  disjabrex  32544  disjabrexf  32545  dfimafnf  32593  curry2ima  32665  cshwrnid  32916  nsgqusf1olem2  33361  pstmval  33861  pstmfval  33862  sigaval  34077  measval  34164  orvcval  34425  bnj956  34742  bnj18eq1  34893  bnj1318  34991  fnrelpredd  35055  derangval  35139  satfdm  35341  fmlasuc  35358  satffunlem1lem2  35375  satffunlem2lem2  35378  mclsval  35535  dfrdg2  35768  dfrdg3  35769  altxpeq1  35946  altxpeq2  35947  ixpeq12dv  36189  cbvcsbdavw  36232  cbvcsbdavw2  36233  cbviundavw  36235  cbviindavw  36236  cbvopab1davw  36237  cbvopab2davw  36238  cbvopabdavw  36239  cbviotadavw  36242  cbvoprab1davw  36244  cbvoprab2davw  36245  cbvoprab3davw  36246  cbvoprab123davw  36247  cbvoprab12davw  36248  cbvoprab23davw  36249  cbvoprab13davw  36250  cbvixpdavw  36251  cbviundavw2  36259  cbviindavw2  36260  cbvixpdavw2  36267  bj-snsetex  36936  bj-sngleq  36940  bj-projeq  36965  bj-projval  36969  bj-imafv  37224  csboprabg  37303  finxpeq1  37359  finxpeq2  37360  csbfinxpg  37361  finxpreclem6  37369  ptrest  37598  poimirlem26  37625  poimirlem27  37626  poimirlem28  37627  mblfinlem3  37638  cnambfre  37647  itg2addnc  37653  areacirclem5  37691  sdclem2  37721  sdc  37723  ismtyval  37779  elghomlem1OLD  37864  iineq12f  38143  eccnvepres  38253  lfl1dim  39099  ldual1dim  39144  glbconxN  39357  lineset  39717  pointsetN  39720  psubspset  39723  pmapglb2xN  39751  polval2N  39885  psubclsetN  39915  lautset  40061  pautsetN  40077  tendofset  40737  tendoset  40738  dva1dim  40964  dia1dim2  41041  dib1dim2  41147  diclspsn  41173  dih1dimatlem  41308  dihglb2  41321  hdmap1ffval  41774  hdmapffval  41805  hgmapffval  41864  sticksstones22  42141  sticksstones23  42142  aks6d1c6isolem3  42149  prjspeclsp  42585  sn-isghm  42646  eldiophb  42730  eldioph  42731  diophrw  42732  eldioph2  42735  eldioph2b  42736  eldioph3  42739  diophin  42745  diophun  42746  diophrex  42748  rexrabdioph  42767  rmxypairf1o  42884  hbtlem1  43096  hbtlem7  43098  tfsconcatrn  43315  nzss  44290  dropab1  44420  dropab2  44421  iineq12dv  45084  supsubc  45333  dfaimafn  47150  dfatsnafv2  47237  rnfdmpr  47266  f1oresf1o  47275  imasetpreimafvbijlemfo  47390  fargshiftfo  47427  sprval  47464  sprvalpw  47465  prprval  47499  prprvalpw  47500  prprspr2  47503  isgrim  47867  isgrlim  47967  setrecseq  49671