Theorem abbidv 2906

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2163, 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

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		abbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	sbbidv 2020	. 2 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
3	2	abbilem 2903	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  {cab 2763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-sb 2012  df-clab 2764  df-cleq 2770

This theorem is referenced by:  abbii  2908  rabbidva2  3383  cdeqab  3642  sbceqbid  3659  csbeq1  3754  csbeq2  3755  csbprc  4206  sbcel12  4208  sbceqg  4209  csbeq2d  4216  csbnestgf  4221  pweq  4382  sneq  4408  csbsng  4475  unieq  4681  csbuni  4703  inteq  4715  iineq1  4770  iineq2  4773  dfiin2g  4788  iinrab  4817  iinxprg  4836  opabbid  4953  imasng  5743  iotaeq  6109  iotabi  6110  dfimafn  6507  fnsnfv  6520  fliftf  6839  oprabbid  6987  wrecseq123  7692  rdglim2  7813  qseq1  8080  qseq2  8081  qsinxp  8108  mapvalg  8152  ixpsnval  8199  ixpeq1  8207  fival  8608  tcvalg  8913  karden  9057  acneq  9201  infmap2  9377  cfval  9406  cflim3  9421  axdclem  9678  axdc  9680  rankcf  9936  genpv  10158  negfi  11330  supadd  11350  hashf1lem2  13560  hashf1  13561  hashfac  13562  csbwrdg  13639  cshimadifsn  13986  cshimadifsn0  13987  cleq1  14137  dfrtrcl2  14215  shftlem  14221  shftfib  14225  vdwlem6  16105  cshwsiun  16216  lubfval  17375  glbfval  17388  eqglact  18040  isghm  18055  symgval  18193  sylow1lem2  18409  sylow3lem1  18437  efgval  18525  dmdprd  18795  ixpsnbasval  19617  aspval2  19755  ressmplbas2  19863  cssval  20436  tgval  21178  clsval2  21273  lpfval  21361  lpval  21362  islocfin  21740  ptval  21793  hauspwpwf1  22210  ptcmplem2  22276  snclseqg  22338  ustval  22425  itg2val  23943  limcfval  24084  plyval  24397  isismt  25902  nb3grprlem1  26745  vtxdun  26846  rgrx0ndm  26958  ewlksfval  26966  wwlksnfiOLD  27296  rusgrnumwwlkb0  27368  eclclwwlkn1  27490  avril1  27911  nmoofval  28206  nmooval  28207  nmoo0  28235  nmopval  29304  nmfnval  29324  iunrdx  29961  disjabrex  29975  disjabrexf  29976  dfimafnf  30018  curry2ima  30069  pstmval  30544  pstmfval  30545  sigaval  30779  measval  30867  orvcval  31126  bnj956  31454  bnj18eq1  31604  bnj1318  31700  derangval  31756  mclsval  32067  dfrdg2  32297  dfrdg3  32298  frecseq123  32374  altxpeq1  32677  altxpeq2  32678  bj-snsetex  33531  bj-sngleq  33535  bj-projeq  33560  bj-projval  33564  bj-imafv  33736  csbwrecsg  33776  csboprabg  33779  finxpeq1  33825  finxpeq2  33826  csbfinxpg  33827  finxpreclem6  33835  ptrest  34043  poimirlem26  34070  poimirlem27  34071  poimirlem28  34072  mblfinlem3  34083  cnambfre  34092  itg2addnc  34098  areacirclem5  34138  sdclem2  34171  sdc  34173  ismtyval  34232  elghomlem1OLD  34317  iineq12f  34604  eccnvepres  34686  lfl1dim  35284  ldual1dim  35329  glbconxN  35541  lineset  35901  pointsetN  35904  psubspset  35907  pmapglb2xN  35935  polval2N  36069  psubclsetN  36099  lautset  36245  pautsetN  36261  tendofset  36921  tendoset  36922  dva1dim  37148  dia1dim2  37225  dib1dim2  37331  diclspsn  37357  dih1dimatlem  37492  dihglb2  37505  hdmap1ffval  37958  hdmapffval  37989  hgmapffval  38048  eldiophb  38294  eldioph  38295  diophrw  38296  eldioph2  38299  eldioph2b  38300  eldioph3  38303  diophin  38310  diophun  38311  diophrex  38313  rexrabdioph  38332  rmxypairf1o  38449  hbtlem1  38666  hbtlem7  38668  nzss  39486  dropab1  39619  dropab2  39620  supsubc  40491  dfaimafn  42220  dfatsnafv2  42307  rnfdmpr  42336  f1oresf1o  42345  f1oresf1o2  42346  fargshiftfo  42424  sprval  42432  sprvalpw  42433  prprval  42467  prprvalpw  42468  prprspr2  42471  setrecseq  43551