Theorem abbidv 2806

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547  {cab 2718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732

This theorem is referenced by:  rabbidva2  3394  cdeqab  3718  sbceqbid  3737  csbeq1  3841  csbeq2  3843  csbeq2d  3844  csbeq2dv  3845  csbprc  4344  sbcel12  4346  sbceqg  4347  csbnestgfw  4357  csbnestgf  4362  pweqALT  4551  sneq  4572  csbsng  4647  uniprg  4861  csbuni  4875  inteq  4887  iineq1  4946  iineq2  4949  iuneq12d  4958  dfiin2g  4967  iinrab  5005  iinxprg  5025  opabbid  5144  opabbidv  5145  axrep6g  5219  imasng  6043  predres  6297  iotaeq  6460  iotabi  6461  dfimafn  6896  fliftf  7266  oprabbid  7428  oprabbidv  7429  frecseq123  8229  csbfrecsg  8231  rdglim2  8368  qseq1  8700  qseq2  8701  snecg  8721  qsinxp  8737  mapvalg  8780  fsetexb  8808  ixpsnval  8845  ixpeq1  8853  fival  9322  tcvalg  9655  karden  9817  acneq  9963  infmap2  10137  cfval  10167  cflim3  10182  axdclem  10439  axdc  10441  rankcf  10698  genpv  10920  negfi  12103  supadd  12122  hashf1lem2  14416  hashf1  14417  hashfac  14418  csbwrdg  14504  cshimadifsn  14789  cshimadifsn0  14790  cleq1  14943  dfrtrcl2  15022  shftlem  15028  shftfib  15032  vdwlem6  16955  cshwsiun  17068  lubfval  18312  glbfval  18325  eqglact  19152  qus0subgbas  19171  isghm  19188  isghmOLD  19189  symgval  19344  sylow1lem2  19572  sylow3lem1  19600  efgval  19690  dmdprd  19973  ixpsnbasval  21205  pzriprnglem10  21472  pzriprnglem11  21473  cssval  21664  aspval2  21880  ressmplbas2  22009  tgval  22945  clsval2  23040  lpfval  23128  lpval  23129  islocfin  23507  ptval  23560  hauspwpwf1  23977  ptcmplem2  24043  snclseqg  24106  ustval  24193  itg2val  25720  limcfval  25864  plyval  26183  addsval  27979  addscom  27983  addsass  28022  addbday  28035  mulsval  28126  mulscom  28156  addsdi  28172  mulsass  28183  mulsunif2lem  28186  precsexlemcbv  28223  precsexlem3  28226  halfcut  28475  pw2cut2  28479  elreno  28508  readdscl  28516  remulscl  28519  isismt  28627  nb3grprlem1  29474  vtxdun  29575  rgrx0ndm  29687  ewlksfval  29695  rusgrnumwwlkb0  30067  eclclwwlkn1  30170  avril1  30558  nmoofval  30858  nmooval  30859  nmoo0  30887  nmopval  31952  nmfnval  31972  iunrdx  32659  iinabrex  32665  disjabrex  32678  disjabrexf  32679  dfimafnf  32735  curry2ima  32808  cshwrnid  33047  nsgqusf1olem2  33504  pstmval  34086  pstmfval  34087  sigaval  34302  measval  34389  orvcval  34649  bnj956  34966  bnj18eq1  35116  bnj1318  35214  fnrelpredd  35279  derangval  35402  satfdm  35604  fmlasuc  35621  satffunlem1lem2  35638  satffunlem2lem2  35641  mclsval  35798  dfrdg2  36028  dfrdg3  36029  altxpeq1  36208  altxpeq2  36209  ixpeq12dv  36451  cbvcsbdavw  36494  cbvcsbdavw2  36495  cbviundavw  36497  cbviindavw  36498  cbvopab1davw  36499  cbvopab2davw  36500  cbvopabdavw  36501  cbviotadavw  36504  cbvoprab1davw  36506  cbvoprab2davw  36507  cbvoprab3davw  36508  cbvoprab123davw  36509  cbvoprab12davw  36510  cbvoprab23davw  36511  cbvoprab13davw  36512  cbvixpdavw  36513  cbviundavw2  36521  cbviindavw2  36522  cbvixpdavw2  36529  bj-snsetex  37323  bj-sngleq  37327  bj-projeq  37352  bj-projval  37356  bj-imafv  37618  csboprabg  37699  finxpeq1  37755  finxpeq2  37756  csbfinxpg  37757  finxpreclem6  37765  ptrest  37993  poimirlem26  38020  poimirlem27  38021  poimirlem28  38022  mblfinlem3  38033  cnambfre  38042  itg2addnc  38048  areacirclem5  38086  sdclem2  38116  sdc  38118  ismtyval  38174  elghomlem1OLD  38259  iineq12f  38538  eccnvepres  38660  ecqmap  38823  lfl1dim  39620  ldual1dim  39665  glbconxN  39877  lineset  40237  pointsetN  40240  psubspset  40243  pmapglb2xN  40271  polval2N  40405  psubclsetN  40435  lautset  40581  pautsetN  40597  tendofset  41257  tendoset  41258  dva1dim  41484  dia1dim2  41561  dib1dim2  41667  diclspsn  41693  dih1dimatlem  41828  dihglb2  41841  hdmap1ffval  42294  hdmapffval  42325  hgmapffval  42384  sticksstones22  42660  sticksstones23  42661  aks6d1c6isolem3  42668  prjspeclsp  43069  sn-isghm  43130  eldiophb  43213  eldioph  43214  diophrw  43215  eldioph2  43218  eldioph2b  43219  eldioph3  43222  diophin  43228  diophun  43229  diophrex  43231  rexrabdioph  43246  rmxypairf1o  43363  hbtlem1  43575  hbtlem7  43577  tfsconcatrn  43794  nzss  44768  dropab1  44897  dropab2  44898  iineq12dv  45560  supsubc  45805  dfaimafn  47635  dfatsnafv2  47722  rnfdmpr  47751  f1oresf1o  47760  imasetpreimafvbijlemfo  47887  fargshiftfo  47924  sprval  47961  sprvalpw  47962  prprval  47996  prprvalpw  47997  prprspr2  48000  isgrim  48380  isgrlim  48480  setrecseq  50182