Theorem abbidv 2803

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542  {cab 2715

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729

This theorem is referenced by:  rabbidva2  3403  cdeqab  3730  sbceqbid  3749  csbeq1  3854  csbeq2  3856  csbeq2d  3857  csbeq2dv  3858  csbprc  4363  sbcel12  4365  sbceqg  4366  csbnestgfw  4376  csbnestgf  4381  pweqALT  4571  sneq  4592  rabsneq  4601  csbsng  4667  uniprg  4881  csbuni  4895  inteq  4907  iineq1  4966  iineq2  4969  iuneq12d  4978  dfiin2g  4988  iinrab  5026  iinxprg  5046  opabbid  5165  opabbidv  5166  axrep6g  5237  imasng  6051  predres  6305  iotaeq  6468  iotabi  6469  dfimafn  6904  fliftf  7271  oprabbid  7433  oprabbidv  7434  frecseq123  8234  csbfrecsg  8236  rdglim2  8373  qseq1  8705  qseq2  8706  snecg  8726  qsinxp  8742  mapvalg  8785  fsetexb  8813  ixpsnval  8850  ixpeq1  8858  fival  9327  tcvalg  9657  karden  9819  acneq  9965  infmap2  10139  cfval  10169  cflim3  10184  axdclem  10441  axdc  10443  rankcf  10700  genpv  10922  negfi  12103  supadd  12122  hashf1lem2  14391  hashf1  14392  hashfac  14393  csbwrdg  14479  cshimadifsn  14764  cshimadifsn0  14765  cleq1  14918  dfrtrcl2  14997  shftlem  15003  shftfib  15007  vdwlem6  16926  cshwsiun  17039  lubfval  18283  glbfval  18296  eqglact  19120  qus0subgbas  19139  isghm  19156  isghmOLD  19157  symgval  19312  sylow1lem2  19540  sylow3lem1  19568  efgval  19658  dmdprd  19941  ixpsnbasval  21172  pzriprnglem10  21457  pzriprnglem11  21458  cssval  21649  aspval2  21866  ressmplbas2  21994  tgval  22911  clsval2  23006  lpfval  23094  lpval  23095  islocfin  23473  ptval  23526  hauspwpwf1  23943  ptcmplem2  24009  snclseqg  24072  ustval  24159  itg2val  25697  limcfval  25841  plyval  26166  addsval  27970  addscom  27974  addsass  28013  addbday  28026  mulsval  28117  mulscom  28147  addsdi  28163  mulsass  28174  mulsunif2lem  28177  precsexlemcbv  28214  precsexlem3  28217  halfcut  28466  pw2cut2  28470  elreno  28499  readdscl  28507  remulscl  28510  isismt  28618  nb3grprlem1  29465  vtxdun  29567  rgrx0ndm  29679  ewlksfval  29687  rusgrnumwwlkb0  30059  eclclwwlkn1  30162  avril1  30550  nmoofval  30849  nmooval  30850  nmoo0  30878  nmopval  31943  nmfnval  31963  iunrdx  32649  iinabrex  32655  disjabrex  32668  disjabrexf  32669  dfimafnf  32725  curry2ima  32798  cshwrnid  33053  nsgqusf1olem2  33506  pstmval  34072  pstmfval  34073  sigaval  34288  measval  34375  orvcval  34635  bnj956  34952  bnj18eq1  35102  bnj1318  35200  fnrelpredd  35266  derangval  35380  satfdm  35582  fmlasuc  35599  satffunlem1lem2  35616  satffunlem2lem2  35619  mclsval  35776  dfrdg2  36006  dfrdg3  36007  altxpeq1  36186  altxpeq2  36187  ixpeq12dv  36429  cbvcsbdavw  36472  cbvcsbdavw2  36473  cbviundavw  36475  cbviindavw  36476  cbvopab1davw  36477  cbvopab2davw  36478  cbvopabdavw  36479  cbviotadavw  36482  cbvoprab1davw  36484  cbvoprab2davw  36485  cbvoprab3davw  36486  cbvoprab123davw  36487  cbvoprab12davw  36488  cbvoprab23davw  36489  cbvoprab13davw  36490  cbvixpdavw  36491  cbviundavw2  36499  cbviindavw2  36500  cbvixpdavw2  36507  bj-snsetex  37205  bj-sngleq  37209  bj-projeq  37234  bj-projval  37238  bj-imafv  37500  csboprabg  37579  finxpeq1  37635  finxpeq2  37636  csbfinxpg  37637  finxpreclem6  37645  ptrest  37864  poimirlem26  37891  poimirlem27  37892  poimirlem28  37893  mblfinlem3  37904  cnambfre  37913  itg2addnc  37919  areacirclem5  37957  sdclem2  37987  sdc  37989  ismtyval  38045  elghomlem1OLD  38130  iineq12f  38409  eccnvepres  38531  ecqmap  38694  lfl1dim  39491  ldual1dim  39536  glbconxN  39748  lineset  40108  pointsetN  40111  psubspset  40114  pmapglb2xN  40142  polval2N  40276  psubclsetN  40306  lautset  40452  pautsetN  40468  tendofset  41128  tendoset  41129  dva1dim  41355  dia1dim2  41432  dib1dim2  41538  diclspsn  41564  dih1dimatlem  41699  dihglb2  41712  hdmap1ffval  42165  hdmapffval  42196  hgmapffval  42255  sticksstones22  42532  sticksstones23  42533  aks6d1c6isolem3  42540  prjspeclsp  42964  sn-isghm  43025  eldiophb  43108  eldioph  43109  diophrw  43110  eldioph2  43113  eldioph2b  43114  eldioph3  43117  diophin  43123  diophun  43124  diophrex  43126  rexrabdioph  43145  rmxypairf1o  43262  hbtlem1  43474  hbtlem7  43476  tfsconcatrn  43693  nzss  44667  dropab1  44796  dropab2  44797  iineq12dv  45459  supsubc  45706  dfaimafn  47519  dfatsnafv2  47606  rnfdmpr  47635  f1oresf1o  47644  imasetpreimafvbijlemfo  47759  fargshiftfo  47796  sprval  47833  sprvalpw  47834  prprval  47868  prprvalpw  47869  prprspr2  47872  isgrim  48236  isgrlim  48336  setrecseq  50038