Theorem abbidv 2807

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730

This theorem is referenced by:  rabbidva2  3409  cdeqab  3705  sbceqbid  3723  csbeq1  3835  csbeq2  3837  csbeq2d  3838  csbprc  4341  sbcel12  4343  sbceqg  4344  csbnestgfw  4354  csbnestgf  4359  pweqALT  4551  sneq  4572  csbsng  4645  unieqOLD  4852  uniprg  4857  csbuni  4871  inteq  4883  iineq1  4942  iineq2  4945  dfiin2g  4962  iinrab  4998  iinxprg  5018  opabbid  5139  opabbidv  5140  imasng  5985  predres  6236  iotaeq  6398  iotabi  6399  dfimafn  6825  fnsnfvOLD  6841  fliftf  7179  oprabbid  7331  oprabbidv  7332  frecseq123  8086  csbfrecsg  8088  wrecseq123OLD  8119  rdglim2  8251  qseq1  8540  qseq2  8541  qsinxp  8570  mapvalg  8613  fsetexb  8640  ixpsnval  8676  ixpeq1  8684  fival  9159  tcvalg  9484  karden  9641  acneq  9787  infmap2  9962  cfval  9991  cflim3  10006  axdclem  10263  axdc  10265  rankcf  10521  genpv  10743  negfi  11912  supadd  11931  hashf1lem2  14158  hashf1  14159  hashfac  14160  csbwrdg  14235  cshimadifsn  14530  cshimadifsn0  14531  cleq1  14682  dfrtrcl2  14761  shftlem  14767  shftfib  14771  vdwlem6  16675  cshwsiun  16789  lubfval  18056  glbfval  18069  eqglact  18795  isghm  18822  symgval  18964  sylow1lem2  19192  sylow3lem1  19220  efgval  19311  dmdprd  19589  ixpsnbasval  20468  cssval  20875  aspval2  21090  ressmplbas2  21216  tgval  22093  clsval2  22189  lpfval  22277  lpval  22278  islocfin  22656  ptval  22709  hauspwpwf1  23126  ptcmplem2  23192  snclseqg  23255  ustval  23342  itg2val  24881  limcfval  25024  plyval  25342  isismt  26883  nb3grprlem1  27735  vtxdun  27836  rgrx0ndm  27948  ewlksfval  27956  rusgrnumwwlkb0  28322  eclclwwlkn1  28425  avril1  28813  nmoofval  29110  nmooval  29111  nmoo0  29139  nmopval  30204  nmfnval  30224  iunrdx  30889  iinabrex  30894  disjabrex  30907  disjabrexf  30908  dfimafnf  30957  curry2ima  31027  cshwrnid  31219  nsgqusf1olem2  31585  pstmval  31831  pstmfval  31832  sigaval  32065  measval  32152  orvcval  32410  bnj956  32742  bnj18eq1  32893  bnj1318  32991  fnrelpredd  33047  derangval  33115  satfdm  33317  fmlasuc  33334  satffunlem1lem2  33351  satffunlem2lem2  33354  mclsval  33511  dfrdg2  33757  dfrdg3  33758  addsval  34112  addscom  34115  altxpeq1  34261  altxpeq2  34262  bj-snsetex  35139  bj-sngleq  35143  bj-projeq  35168  bj-projval  35172  bj-imafv  35408  csboprabg  35487  finxpeq1  35543  finxpeq2  35544  csbfinxpg  35545  finxpreclem6  35553  ptrest  35762  poimirlem26  35789  poimirlem27  35790  poimirlem28  35791  mblfinlem3  35802  cnambfre  35811  itg2addnc  35817  areacirclem5  35855  sdclem2  35886  sdc  35888  ismtyval  35944  elghomlem1OLD  36029  iineq12f  36308  eccnvepres  36401  lfl1dim  37121  ldual1dim  37166  glbconxN  37378  lineset  37738  pointsetN  37741  psubspset  37744  pmapglb2xN  37772  polval2N  37906  psubclsetN  37936  lautset  38082  pautsetN  38098  tendofset  38758  tendoset  38759  dva1dim  38985  dia1dim2  39062  dib1dim2  39168  diclspsn  39194  dih1dimatlem  39329  dihglb2  39342  hdmap1ffval  39795  hdmapffval  39826  hgmapffval  39885  sticksstones22  40110  prjspeclsp  40437  eldiophb  40565  eldioph  40566  diophrw  40567  eldioph2  40570  eldioph2b  40571  eldioph3  40574  diophin  40580  diophun  40581  diophrex  40583  rexrabdioph  40602  rmxypairf1o  40719  hbtlem1  40934  hbtlem7  40936  nzss  41894  dropab1  42024  dropab2  42025  supsubc  42851  dfaimafn  44613  dfatsnafv2  44700  rnfdmpr  44729  f1oresf1o  44738  imasetpreimafvbijlemfo  44813  fargshiftfo  44850  sprval  44887  sprvalpw  44888  prprval  44922  prprvalpw  44923  prprspr2  44926  setrecseq  46347