Theorem abbidv 2811

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732

This theorem is referenced by:  rabbidva2  3445  cdeqab  3792  sbceqbid  3811  csbeq1  3924  csbeq2  3926  csbeq2d  3927  csbeq2dv  3928  csbprc  4432  sbcel12  4434  sbceqg  4435  csbnestgfw  4445  csbnestgf  4450  pweqALT  4637  sneq  4658  rabsneq  4666  csbsng  4733  uniprg  4947  csbuni  4960  inteq  4973  iineq1  5032  iineq2  5035  iuneq12d  5044  dfiin2g  5055  iinrab  5092  iinxprg  5112  opabbid  5231  opabbidv  5232  axrep6g  5311  imasng  6113  predres  6371  iotaeq  6538  iotabi  6539  dfimafn  6984  fliftf  7351  oprabbid  7515  oprabbidv  7516  frecseq123  8323  csbfrecsg  8325  wrecseq123OLD  8356  rdglim2  8488  qseq1  8819  qseq2  8820  qsinxp  8851  mapvalg  8894  fsetexb  8922  ixpsnval  8958  ixpeq1  8966  fival  9481  tcvalg  9807  karden  9964  acneq  10112  infmap2  10286  cfval  10316  cflim3  10331  axdclem  10588  axdc  10590  rankcf  10846  genpv  11068  negfi  12244  supadd  12263  hashf1lem2  14505  hashf1  14506  hashfac  14507  csbwrdg  14592  cshimadifsn  14878  cshimadifsn0  14879  cleq1  15032  dfrtrcl2  15111  shftlem  15117  shftfib  15121  vdwlem6  17033  cshwsiun  17147  lubfval  18420  glbfval  18433  eqglact  19219  qus0subgbas  19238  isghm  19255  isghmOLD  19256  symgval  19412  sylow1lem2  19641  sylow3lem1  19669  efgval  19759  dmdprd  20042  ixpsnbasval  21238  pzriprnglem10  21524  pzriprnglem11  21525  cssval  21723  aspval2  21941  ressmplbas2  22068  tgval  22983  clsval2  23079  lpfval  23167  lpval  23168  islocfin  23546  ptval  23599  hauspwpwf1  24016  ptcmplem2  24082  snclseqg  24145  ustval  24232  itg2val  25783  limcfval  25927  plyval  26252  addsval  28013  addscom  28017  addsass  28056  addsbday  28068  mulsval  28153  mulscom  28183  addsdi  28199  mulsass  28210  mulsunif2lem  28213  precsexlemcbv  28248  precsexlem3  28251  halfcut  28434  elreno  28445  readdscl  28449  remulscl  28452  isismt  28560  nb3grprlem1  29415  vtxdun  29517  rgrx0ndm  29629  ewlksfval  29637  rusgrnumwwlkb0  30004  eclclwwlkn1  30107  avril1  30495  nmoofval  30794  nmooval  30795  nmoo0  30823  nmopval  31888  nmfnval  31908  iunrdx  32586  iinabrex  32591  disjabrex  32604  disjabrexf  32605  dfimafnf  32655  curry2ima  32720  cshwrnid  32928  nsgqusf1olem2  33407  pstmval  33841  pstmfval  33842  sigaval  34075  measval  34162  orvcval  34422  bnj956  34752  bnj18eq1  34903  bnj1318  35001  fnrelpredd  35065  derangval  35135  satfdm  35337  fmlasuc  35354  satffunlem1lem2  35371  satffunlem2lem2  35374  mclsval  35531  dfrdg2  35759  dfrdg3  35760  altxpeq1  35937  altxpeq2  35938  ixpeq12dv  36182  cbvcsbdavw  36225  cbvcsbdavw2  36226  cbviundavw  36228  cbviindavw  36229  cbvopab1davw  36230  cbvopab2davw  36231  cbvopabdavw  36232  cbviotadavw  36235  cbvoprab1davw  36237  cbvoprab2davw  36238  cbvoprab3davw  36239  cbvoprab123davw  36240  cbvoprab12davw  36241  cbvoprab23davw  36242  cbvoprab13davw  36243  cbvixpdavw  36244  cbviundavw2  36252  cbviindavw2  36253  cbvixpdavw2  36260  bj-snsetex  36929  bj-sngleq  36933  bj-projeq  36958  bj-projval  36962  bj-imafv  37217  csboprabg  37296  finxpeq1  37352  finxpeq2  37353  csbfinxpg  37354  finxpreclem6  37362  ptrest  37579  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  mblfinlem3  37619  cnambfre  37628  itg2addnc  37634  areacirclem5  37672  sdclem2  37702  sdc  37704  ismtyval  37760  elghomlem1OLD  37845  iineq12f  38124  eccnvepres  38236  lfl1dim  39077  ldual1dim  39122  glbconxN  39335  lineset  39695  pointsetN  39698  psubspset  39701  pmapglb2xN  39729  polval2N  39863  psubclsetN  39893  lautset  40039  pautsetN  40055  tendofset  40715  tendoset  40716  dva1dim  40942  dia1dim2  41019  dib1dim2  41125  diclspsn  41151  dih1dimatlem  41286  dihglb2  41299  hdmap1ffval  41752  hdmapffval  41783  hgmapffval  41842  sticksstones22  42125  sticksstones23  42126  aks6d1c6isolem3  42133  prjspeclsp  42567  sn-isghm  42628  eldiophb  42713  eldioph  42714  diophrw  42715  eldioph2  42718  eldioph2b  42719  eldioph3  42722  diophin  42728  diophun  42729  diophrex  42731  rexrabdioph  42750  rmxypairf1o  42868  hbtlem1  43080  hbtlem7  43082  tfsconcatrn  43304  nzss  44286  dropab1  44416  dropab2  44417  iineq12dv  45008  supsubc  45268  dfaimafn  47080  dfatsnafv2  47167  rnfdmpr  47196  f1oresf1o  47205  imasetpreimafvbijlemfo  47279  fargshiftfo  47316  sprval  47353  sprvalpw  47354  prprval  47388  prprvalpw  47389  prprspr2  47392  isgrim  47752  isgrlim  47806  setrecseq  48777