Theorem abbidv 2826

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752

This theorem is used by:  rabbidva2  3414  cdeqab  3727  sbceqbid  3745  csbeq1  3849  csbeq2  3851  csbeq2d  3852  csbeq2dv  3853  csbprc  4366  sbcel12  4368  sbceqg  4369  csbnestgfw  4379  csbnestgf  4384  pweqALT  4571  sneq  4590  csbsng  4665  uniprg  4882  csbuni  4897  inteq  4909  iineq1  4968  iineq2  4971  iuneq12d  4979  dfiin2g  4988  iinrab  5026  iinxprg  5048  opabbid  5169  opabbidv  5170  axrep6g  5242  dfrn7  6065  imasng  6081  predres  6342  iotaeq  6506  iotabi  6507  dfimafn  6947  fliftf  7323  oprabbid  7485  oprabbidv  7486  frecseq123  8303  csbfrecsg  8305  rdglim2  8443  qseq1  8780  qseq2  8781  snecg  8801  qsinxp  8817  mapvalg  8859  fsetexb  8889  ixpsnval  8931  ixpeq1  8939  fival  9407  tcvalg  9740  karden  9962  kardenOLD  9963  acneq  10125  infmap2  10298  cfval  10327  cflim3  10343  axdclem  10600  axdc  10602  rankcf  10865  genpv  11087  negfi  12269  supadd  12288  hashf1lem2  14604  hashf1  14605  hashfac  14606  csbwrdg  14692  cshimadifsn  14984  cshimadifsn0  14985  cleq1  15141  dfrtrcl2  15220  shftlem  15226  shftfib  15230  vdwlem6  17169  cshwsiun  17282  lubfval  18527  glbfval  18540  eqglact  19396  qus0subgbas  19418  isghm  19435  symgval  19590  sylow1lem2  19818  sylow3lem1  19846  efgval  19936  dmdprd  20219  ixpsnbasval  21488  pzriprnglem10  21801  pzriprnglem11  21802  cssval  21993  aspval2  22211  ressmplbas2  22340  tgval  23278  clsval2  23373  lpfval  23461  lpval  23462  islocfin  23841  ptval  23894  hauspwpwf1  24311  ptcmplem2  24377  snclseqg  24440  ustval  24527  itg2val  26054  limcfval  26197  plyval  26516  addsval  28353  addscom  28357  addsass  28396  addbday  28409  mulsval  28500  mulscom  28530  addsdi  28546  mulsass  28557  mulsunif2lem  28560  precsexlemcbv  28597  precsexlem3  28600  halfcut  28849  pw2cut2  28853  elreno  28882  readdscl  28890  remulscl  28893  isismt  29002  nb3grprlem1  29966  vtxdun  30067  rgrx0ndm  30179  ewlksfval  30187  rusgrnumwwlkb0  30568  eclclwwlkn1  30671  avril1  31069  nmoofval  31369  nmooval  31370  nmoo0  31398  nmopval  32463  nmfnval  32483  iunrdx  33205  iinabrex  33210  disjabrex  33223  disjabrexf  33224  dfimafnf  33277  curry2ima  33349  cshwrnid  33568  nsgqusf1olem2  34011  pstmval  34573  pstmfval  34574  sigaval  34789  measval  34877  orvcval  35136  bnj956  35453  bnj18eq1  35603  bnj1318  35701  fnrelpredd  35772  kardval  35876  kard0  35878  derangval  36018  satfdm  36220  fmlasuc  36237  satffunlem1lem2  36254  satffunlem2lem2  36257  mclsval  36414  dfrdg2  36649  dfrdg3  36650  altxpeq1  36830  altxpeq2  36831  ixpeq12dv  37097  cbvcsbdavw  37140  cbvcsbdavw2  37141  cbviundavw  37143  cbviindavw  37144  cbvopab1davw  37145  cbvopab2davw  37146  cbvopabdavw  37147  cbviotadavw  37150  cbvoprab1davw  37152  cbvoprab2davw  37153  cbvoprab3davw  37154  cbvoprab123davw  37155  cbvoprab12davw  37156  cbvoprab23davw  37157  cbvoprab13davw  37158  cbvixpdavw  37159  cbviundavw2  37167  cbviindavw2  37168  cbvixpdavw2  37175  bj-snsetex  37968  bj-sngleq  37972  bj-projeq  37997  bj-projval  38001  bj-imafv  38265  csboprabg  38346  finxpeq1  38402  finxpeq2  38403  csbfinxpg  38404  finxpreclem6  38412  ptrest  38630  poimirlem26  38657  poimirlem27  38658  poimirlem28  38659  mblfinlem3  38670  cnambfre  38679  itg2addnc  38685  areacirclem5  38723  varprop  38735  negprop  38736  impprop  38737  dfprop2  38739  sdclem2  38769  sdc  38771  ismtyval  38827  elghomlem1OLD  38912  iineq12f  39189  eccnvepres  39311  ecqmap  39474  lfl1dim  40271  ldual1dim  40316  glbconxN  40528  lineset  40888  pointsetN  40891  psubspset  40894  pmapglb2xN  40922  polval2N  41056  psubclsetN  41086  lautset  41232  pautsetN  41248  tendofset  41908  tendoset  41909  dva1dim  42135  dia1dim2  42212  dib1dim2  42318  diclspsn  42344  dih1dimatlem  42479  dihglb2  42492  hdmap1ffval  42945  hdmapffval  42976  hgmapffval  43035  sticksstones22  43311  sticksstones23  43312  aks6d1c6isolem3  43319  prjspeclsp  43733  sn-isghm  43777  eldiophb  43861  eldioph  43862  diophrw  43863  eldioph2  43866  eldioph2b  43867  eldioph3  43870  diophin  43876  diophun  43877  diophrex  43879  rexrabdioph  43894  rmxypairf1o  44011  hbtlem1  44218  hbtlem7  44220  tfsconcatrn  44437  nzss  45394  dropab1  45523  dropab2  45524  iineq12dv  46214  supsubc  46458  dfaimafn  48328  dfatsnafv2  48415  rnfdmpr  48444  f1oresf1o  48453  imasetpreimafvbijlemfo  48580  fargshiftfo  48617  sprval  48654  sprvalpw  48655  prprval  48689  prprvalpw  48690  prprspr2  48693  isgrim  49073  isgrlim  49173  setrecseq  50956