Theorem abbidv 2800

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1537   = wceq 1539  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726

This theorem is referenced by:  rabbidva2  3421  cdeqab  3758  sbceqbid  3777  csbeq1  3882  csbeq2  3884  csbeq2d  3885  csbeq2dv  3886  csbprc  4389  sbcel12  4391  sbceqg  4392  csbnestgfw  4402  csbnestgf  4407  pweqALT  4595  sneq  4616  rabsneq  4624  csbsng  4688  uniprg  4903  csbuni  4916  inteq  4929  iineq1  4989  iineq2  4992  iuneq12d  5001  dfiin2g  5012  iinrab  5049  iinxprg  5069  opabbid  5188  opabbidv  5189  axrep6g  5270  imasng  6082  predres  6339  iotaeq  6506  iotabi  6507  dfimafn  6951  fliftf  7317  oprabbid  7480  oprabbidv  7481  frecseq123  8289  csbfrecsg  8291  wrecseq123OLD  8322  rdglim2  8454  qseq1  8783  qseq2  8784  qsinxp  8815  mapvalg  8858  fsetexb  8886  ixpsnval  8922  ixpeq1  8930  fival  9434  tcvalg  9760  karden  9917  acneq  10065  infmap2  10239  cfval  10269  cflim3  10284  axdclem  10541  axdc  10543  rankcf  10799  genpv  11021  negfi  12199  supadd  12218  hashf1lem2  14477  hashf1  14478  hashfac  14479  csbwrdg  14564  cshimadifsn  14850  cshimadifsn0  14851  cleq1  15004  dfrtrcl2  15083  shftlem  15089  shftfib  15093  vdwlem6  17006  cshwsiun  17119  lubfval  18364  glbfval  18377  eqglact  19166  qus0subgbas  19185  isghm  19202  isghmOLD  19203  symgval  19356  sylow1lem2  19585  sylow3lem1  19613  efgval  19703  dmdprd  19986  ixpsnbasval  21177  pzriprnglem10  21463  pzriprnglem11  21464  cssval  21654  aspval2  21872  ressmplbas2  21999  tgval  22909  clsval2  23004  lpfval  23092  lpval  23093  islocfin  23471  ptval  23524  hauspwpwf1  23941  ptcmplem2  24007  snclseqg  24070  ustval  24157  itg2val  25699  limcfval  25843  plyval  26168  addsval  27931  addscom  27935  addsass  27974  addsbday  27986  mulsval  28071  mulscom  28101  addsdi  28117  mulsass  28128  mulsunif2lem  28131  precsexlemcbv  28166  precsexlem3  28169  halfcut  28352  elreno  28363  readdscl  28367  remulscl  28370  isismt  28478  nb3grprlem1  29325  vtxdun  29427  rgrx0ndm  29539  ewlksfval  29547  rusgrnumwwlkb0  29919  eclclwwlkn1  30022  avril1  30410  nmoofval  30709  nmooval  30710  nmoo0  30738  nmopval  31803  nmfnval  31823  iunrdx  32511  iinabrex  32517  disjabrex  32530  disjabrexf  32531  dfimafnf  32581  curry2ima  32653  cshwrnid  32886  nsgqusf1olem2  33377  pstmval  33853  pstmfval  33854  sigaval  34071  measval  34158  orvcval  34419  bnj956  34749  bnj18eq1  34900  bnj1318  34998  fnrelpredd  35062  derangval  35131  satfdm  35333  fmlasuc  35350  satffunlem1lem2  35367  satffunlem2lem2  35370  mclsval  35527  dfrdg2  35755  dfrdg3  35756  altxpeq1  35933  altxpeq2  35934  ixpeq12dv  36176  cbvcsbdavw  36219  cbvcsbdavw2  36220  cbviundavw  36222  cbviindavw  36223  cbvopab1davw  36224  cbvopab2davw  36225  cbvopabdavw  36226  cbviotadavw  36229  cbvoprab1davw  36231  cbvoprab2davw  36232  cbvoprab3davw  36233  cbvoprab123davw  36234  cbvoprab12davw  36235  cbvoprab23davw  36236  cbvoprab13davw  36237  cbvixpdavw  36238  cbviundavw2  36246  cbviindavw2  36247  cbvixpdavw2  36254  bj-snsetex  36923  bj-sngleq  36927  bj-projeq  36952  bj-projval  36956  bj-imafv  37211  csboprabg  37290  finxpeq1  37346  finxpeq2  37347  csbfinxpg  37348  finxpreclem6  37356  ptrest  37585  poimirlem26  37612  poimirlem27  37613  poimirlem28  37614  mblfinlem3  37625  cnambfre  37634  itg2addnc  37640  areacirclem5  37678  sdclem2  37708  sdc  37710  ismtyval  37766  elghomlem1OLD  37851  iineq12f  38130  eccnvepres  38240  lfl1dim  39081  ldual1dim  39126  glbconxN  39339  lineset  39699  pointsetN  39702  psubspset  39705  pmapglb2xN  39733  polval2N  39867  psubclsetN  39897  lautset  40043  pautsetN  40059  tendofset  40719  tendoset  40720  dva1dim  40946  dia1dim2  41023  dib1dim2  41129  diclspsn  41155  dih1dimatlem  41290  dihglb2  41303  hdmap1ffval  41756  hdmapffval  41787  hgmapffval  41846  sticksstones22  42128  sticksstones23  42129  aks6d1c6isolem3  42136  prjspeclsp  42585  sn-isghm  42646  eldiophb  42731  eldioph  42732  diophrw  42733  eldioph2  42736  eldioph2b  42737  eldioph3  42740  diophin  42746  diophun  42747  diophrex  42749  rexrabdioph  42768  rmxypairf1o  42886  hbtlem1  43098  hbtlem7  43100  tfsconcatrn  43317  nzss  44293  dropab1  44423  dropab2  44424  iineq12dv  45068  supsubc  45321  dfaimafn  47135  dfatsnafv2  47222  rnfdmpr  47251  f1oresf1o  47260  imasetpreimafvbijlemfo  47350  fargshiftfo  47387  sprval  47424  sprvalpw  47425  prprval  47459  prprvalpw  47460  prprspr2  47463  isgrim  47826  isgrlim  47907  setrecseq  49212