Theorem abbidv 2827

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  {cab 2739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753

This theorem is used by:  rabbidva2  3415  cdeqab  3728  sbceqbid  3746  csbeq1  3850  csbeq2  3852  csbeq2d  3853  csbeq2dv  3854  csbprc  4367  sbcel12  4369  sbceqg  4370  csbnestgfw  4380  csbnestgf  4385  pweqALT  4572  sneq  4594  csbsng  4669  uniprg  4883  csbuni  4898  inteq  4910  iineq1  4969  iineq2  4972  iuneq12d  4980  dfiin2g  4989  iinrab  5027  iinxprg  5049  opabbid  5170  opabbidv  5171  axrep6g  5243  imasng  6078  predres  6335  iotaeq  6499  iotabi  6500  dfimafn  6939  fliftf  7315  oprabbid  7477  oprabbidv  7478  frecseq123  8284  csbfrecsg  8286  rdglim2  8424  qseq1  8761  qseq2  8762  snecg  8782  qsinxp  8798  mapvalg  8840  fsetexb  8870  ixpsnval  8912  ixpeq1  8920  fival  9388  tcvalg  9721  karden  9940  kardenOLD  9941  acneq  10103  infmap2  10276  cfval  10305  cflim3  10321  axdclem  10578  axdc  10580  rankcf  10843  genpv  11065  negfi  12247  supadd  12266  hashf1lem2  14581  hashf1  14582  hashfac  14583  csbwrdg  14669  cshimadifsn  14960  cshimadifsn0  14961  cleq1  15116  dfrtrcl2  15195  shftlem  15201  shftfib  15205  vdwlem6  17144  cshwsiun  17257  lubfval  18502  glbfval  18515  eqglact  19371  qus0subgbas  19393  isghm  19410  symgval  19565  sylow1lem2  19793  sylow3lem1  19821  efgval  19911  dmdprd  20194  ixpsnbasval  21463  pzriprnglem10  21776  pzriprnglem11  21777  cssval  21968  aspval2  22186  ressmplbas2  22315  tgval  23253  clsval2  23348  lpfval  23436  lpval  23437  islocfin  23816  ptval  23869  hauspwpwf1  24286  ptcmplem2  24352  snclseqg  24415  ustval  24502  itg2val  26029  limcfval  26172  plyval  26491  addsval  28330  addscom  28334  addsass  28373  addbday  28386  mulsval  28477  mulscom  28507  addsdi  28523  mulsass  28534  mulsunif2lem  28537  precsexlemcbv  28574  precsexlem3  28577  halfcut  28826  pw2cut2  28830  elreno  28859  readdscl  28867  remulscl  28870  isismt  28979  nb3grprlem1  29943  vtxdun  30044  rgrx0ndm  30156  ewlksfval  30164  rusgrnumwwlkb0  30545  eclclwwlkn1  30648  avril1  31046  nmoofval  31346  nmooval  31347  nmoo0  31375  nmopval  32440  nmfnval  32460  iunrdx  33140  iinabrex  33145  disjabrex  33158  disjabrexf  33159  dfimafnf  33212  curry2ima  33284  cshwrnid  33504  nsgqusf1olem2  33947  pstmval  34509  pstmfval  34510  sigaval  34725  measval  34813  orvcval  35073  bnj956  35390  bnj18eq1  35540  bnj1318  35638  fnrelpredd  35699  kardval  35793  kard0  35795  derangval  35901  satfdm  36103  fmlasuc  36120  satffunlem1lem2  36137  satffunlem2lem2  36140  mclsval  36297  dfrdg2  36527  dfrdg3  36528  altxpeq1  36708  altxpeq2  36709  ixpeq12dv  36975  cbvcsbdavw  37018  cbvcsbdavw2  37019  cbviundavw  37021  cbviindavw  37022  cbvopab1davw  37023  cbvopab2davw  37024  cbvopabdavw  37025  cbviotadavw  37028  cbvoprab1davw  37030  cbvoprab2davw  37031  cbvoprab3davw  37032  cbvoprab123davw  37033  cbvoprab12davw  37034  cbvoprab23davw  37035  cbvoprab13davw  37036  cbvixpdavw  37037  cbviundavw2  37045  cbviindavw2  37046  cbvixpdavw2  37053  bj-snsetex  37846  bj-sngleq  37850  bj-projeq  37875  bj-projval  37879  bj-imafv  38140  csboprabg  38221  finxpeq1  38277  finxpeq2  38278  csbfinxpg  38279  finxpreclem6  38287  ptrest  38505  poimirlem26  38532  poimirlem27  38533  poimirlem28  38534  mblfinlem3  38545  cnambfre  38554  itg2addnc  38560  areacirclem5  38598  varprop  38610  negprop  38611  impprop  38612  dfprop2  38614  sdclem2  38644  sdc  38646  ismtyval  38702  elghomlem1OLD  38787  iineq12f  39064  eccnvepres  39186  ecqmap  39349  lfl1dim  40146  ldual1dim  40191  glbconxN  40403  lineset  40763  pointsetN  40766  psubspset  40769  pmapglb2xN  40797  polval2N  40931  psubclsetN  40961  lautset  41107  pautsetN  41123  tendofset  41783  tendoset  41784  dva1dim  42010  dia1dim2  42087  dib1dim2  42193  diclspsn  42219  dih1dimatlem  42354  dihglb2  42367  hdmap1ffval  42820  hdmapffval  42851  hgmapffval  42910  sticksstones22  43186  sticksstones23  43187  aks6d1c6isolem3  43194  prjspeclsp  43602  sn-isghm  43638  eldiophb  43721  eldioph  43722  diophrw  43723  eldioph2  43726  eldioph2b  43727  eldioph3  43730  diophin  43736  diophun  43737  diophrex  43739  rexrabdioph  43754  rmxypairf1o  43871  hbtlem1  44083  hbtlem7  44085  tfsconcatrn  44302  nzss  45260  dropab1  45389  dropab2  45390  iineq12dv  46064  supsubc  46309  dfaimafn  48179  dfatsnafv2  48266  rnfdmpr  48295  f1oresf1o  48304  imasetpreimafvbijlemfo  48431  fargshiftfo  48468  sprval  48505  sprvalpw  48506  prprval  48540  prprvalpw  48541  prprspr2  48544  isgrim  48924  isgrlim  49024  setrecseq  50732