Theorem abbidv 2862

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538  {cab 2776

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791

This theorem is referenced by:  rabbidva2  3423  cdeqab  3709  sbceqbid  3727  csbeq1  3831  csbeq2  3833  csbeq2d  3834  csbprc  4313  sbcel12  4316  sbceqg  4317  csbnestgfw  4327  csbnestgf  4332  pweqALT  4514  sneq  4535  csbsng  4604  opeq1  4763  opeq2  4765  unieqOLD  4812  csbuni  4829  inteq  4841  iineq1  4898  iineq2  4901  dfiin2g  4919  iinrab  4954  iinxprg  4974  opabbid  5095  imasng  5918  iotaeq  6295  iotabi  6296  dfimafn  6703  fnsnfv  6718  fliftf  7047  oprabbid  7198  wrecseq123  7931  rdglim2  8051  qseq1  8326  qseq2  8327  qsinxp  8356  mapvalg  8399  ixpsnval  8447  ixpeq1  8455  fival  8860  tcvalg  9164  karden  9308  acneq  9454  infmap2  9629  cfval  9658  cflim3  9673  axdclem  9930  axdc  9932  rankcf  10188  genpv  10410  negfi  11577  supadd  11596  hashf1lem2  13810  hashf1  13811  hashfac  13812  csbwrdg  13887  cshimadifsn  14182  cshimadifsn0  14183  cleq1  14334  dfrtrcl2  14413  shftlem  14419  shftfib  14423  vdwlem6  16312  cshwsiun  16425  lubfval  17580  glbfval  17593  eqglact  18323  isghm  18350  symgval  18489  sylow1lem2  18716  sylow3lem1  18744  efgval  18835  dmdprd  19113  ixpsnbasval  19975  cssval  20371  aspval2  20584  ressmplbas2  20695  tgval  21560  clsval2  21655  lpfval  21743  lpval  21744  islocfin  22122  ptval  22175  hauspwpwf1  22592  ptcmplem2  22658  snclseqg  22721  ustval  22808  itg2val  24332  limcfval  24475  plyval  24790  isismt  26328  nb3grprlem1  27170  vtxdun  27271  rgrx0ndm  27383  ewlksfval  27391  rusgrnumwwlkb0  27757  eclclwwlkn1  27860  avril1  28248  nmoofval  28545  nmooval  28546  nmoo0  28574  nmopval  29639  nmfnval  29659  iunrdx  30327  iinabrex  30332  disjabrex  30345  disjabrexf  30346  dfimafnf  30395  curry2ima  30468  cshwrnid  30661  pstmval  31248  pstmfval  31249  sigaval  31480  measval  31567  orvcval  31825  bnj956  32158  bnj18eq1  32309  bnj1318  32407  fnrelpredd  32472  derangval  32527  satfdm  32729  fmlasuc  32746  satffunlem1lem2  32763  satffunlem2lem2  32766  mclsval  32923  dfrdg2  33153  dfrdg3  33154  frecseq123  33232  altxpeq1  33547  altxpeq2  33548  bj-snsetex  34399  bj-sngleq  34403  bj-projeq  34428  bj-projval  34432  bj-imafv  34666  csbwrecsg  34744  csboprabg  34747  finxpeq1  34803  finxpeq2  34804  csbfinxpg  34805  finxpreclem6  34813  ptrest  35056  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  mblfinlem3  35096  cnambfre  35105  itg2addnc  35111  areacirclem5  35149  sdclem2  35180  sdc  35182  ismtyval  35238  elghomlem1OLD  35323  iineq12f  35602  eccnvepres  35697  lfl1dim  36417  ldual1dim  36462  glbconxN  36674  lineset  37034  pointsetN  37037  psubspset  37040  pmapglb2xN  37068  polval2N  37202  psubclsetN  37232  lautset  37378  pautsetN  37394  tendofset  38054  tendoset  38055  dva1dim  38281  dia1dim2  38358  dib1dim2  38464  diclspsn  38490  dih1dimatlem  38625  dihglb2  38638  hdmap1ffval  39091  hdmapffval  39122  hgmapffval  39181  prjspeclsp  39606  eldiophb  39698  eldioph  39699  diophrw  39700  eldioph2  39703  eldioph2b  39704  eldioph3  39707  diophin  39713  diophun  39714  diophrex  39716  rexrabdioph  39735  rmxypairf1o  39852  hbtlem1  40067  hbtlem7  40069  nzss  41021  dropab1  41151  dropab2  41152  supsubc  41985  dfaimafn  43721  dfatsnafv2  43808  rnfdmpr  43837  f1oresf1o  43846  imasetpreimafvbijlemfo  43922  fargshiftfo  43959  sprval  43996  sprvalpw  43997  prprval  44031  prprvalpw  44032  prprspr2  44035  setrecseq  45215