Theorem abbidv 2832

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  rabbidva2  3421  cdeqab  3736  sbceqbid  3754  csbeq1  3859  csbeq2  3861  csbeq2d  3862  csbeq2dv  3863  csbprc  4377  sbcel12  4379  sbceqg  4380  csbnestgfw  4390  csbnestgf  4395  pweqALT  4582  sneq  4604  csbsng  4679  uniprg  4893  csbuni  4908  inteq  4920  iineq1  4979  iineq2  4982  iuneq12d  4991  dfiin2g  5000  iinrab  5038  iinxprg  5060  opabbid  5181  opabbidv  5182  axrep6g  5256  imasng  6091  predres  6347  iotaeq  6511  iotabi  6512  dfimafn  6950  fliftf  7324  oprabbid  7488  oprabbidv  7489  frecseq123  8288  csbfrecsg  8290  rdglim2  8428  qseq1  8763  qseq2  8764  snecg  8784  qsinxp  8800  mapvalg  8842  fsetexb  8870  ixpsnval  8907  ixpeq1  8915  fival  9382  tcvalg  9715  karden  9898  kardenOLD  9899  acneq  10046  infmap2  10219  cfval  10248  cflim3  10264  axdclem  10521  axdc  10523  rankcf  10780  genpv  11002  negfi  12182  supadd  12201  hashf1lem2  14513  hashf1  14514  hashfac  14515  csbwrdg  14601  cshimadifsn  14892  cshimadifsn0  14893  cleq1  15046  dfrtrcl2  15125  shftlem  15131  shftfib  15135  vdwlem6  17071  cshwsiun  17184  lubfval  18429  glbfval  18442  eqglact  19278  qus0subgbas  19300  isghm  19317  symgval  19472  sylow1lem2  19700  sylow3lem1  19728  efgval  19818  dmdprd  20101  ixpsnbasval  21366  pzriprnglem10  21677  pzriprnglem11  21678  cssval  21869  aspval2  22085  ressmplbas2  22214  tgval  23149  clsval2  23244  lpfval  23332  lpval  23333  islocfin  23711  ptval  23764  hauspwpwf1  24181  ptcmplem2  24247  snclseqg  24310  ustval  24397  itg2val  25924  limcfval  26068  plyval  26387  addsval  28192  addscom  28196  addsass  28235  addbday  28248  mulsval  28339  mulscom  28369  addsdi  28385  mulsass  28396  mulsunif2lem  28399  precsexlemcbv  28436  precsexlem3  28439  halfcut  28688  pw2cut2  28692  elreno  28721  readdscl  28729  remulscl  28732  isismt  28840  nb3grprlem1  29767  vtxdun  29868  rgrx0ndm  29980  ewlksfval  29988  rusgrnumwwlkb0  30360  eclclwwlkn1  30463  avril1  30851  nmoofval  31151  nmooval  31152  nmoo0  31180  nmopval  32245  nmfnval  32265  iunrdx  32945  iinabrex  32951  disjabrex  32964  disjabrexf  32965  dfimafnf  33018  curry2ima  33091  cshwrnid  33312  nsgqusf1olem2  33754  pstmval  34316  pstmfval  34317  sigaval  34532  measval  34620  orvcval  34880  bnj956  35197  bnj18eq1  35347  bnj1318  35445  fnrelpredd  35507  kardval  35589  kard0  35591  derangval  35680  satfdm  35882  fmlasuc  35899  satffunlem1lem2  35916  satffunlem2lem2  35919  mclsval  36076  dfrdg2  36306  dfrdg3  36307  altxpeq1  36486  altxpeq2  36487  ixpeq12dv  36769  cbvcsbdavw  36812  cbvcsbdavw2  36813  cbviundavw  36815  cbviindavw  36816  cbvopab1davw  36817  cbvopab2davw  36818  cbvopabdavw  36819  cbviotadavw  36822  cbvoprab1davw  36824  cbvoprab2davw  36825  cbvoprab3davw  36826  cbvoprab123davw  36827  cbvoprab12davw  36828  cbvoprab23davw  36829  cbvoprab13davw  36830  cbvixpdavw  36831  cbviundavw2  36839  cbviindavw2  36840  cbvixpdavw2  36847  bj-snsetex  37640  bj-sngleq  37644  bj-projeq  37669  bj-projval  37673  bj-imafv  37936  csboprabg  38017  finxpeq1  38073  finxpeq2  38074  csbfinxpg  38075  finxpreclem6  38083  ptrest  38311  poimirlem26  38338  poimirlem27  38339  poimirlem28  38340  mblfinlem3  38351  cnambfre  38360  itg2addnc  38366  areacirclem5  38404  sdclem2  38434  sdc  38436  ismtyval  38492  elghomlem1OLD  38577  iineq12f  38854  eccnvepres  38976  ecqmap  39139  lfl1dim  39936  ldual1dim  39981  glbconxN  40193  lineset  40553  pointsetN  40556  psubspset  40559  pmapglb2xN  40587  polval2N  40721  psubclsetN  40751  lautset  40897  pautsetN  40913  tendofset  41573  tendoset  41574  dva1dim  41800  dia1dim2  41877  dib1dim2  41983  diclspsn  42009  dih1dimatlem  42144  dihglb2  42157  hdmap1ffval  42610  hdmapffval  42641  hgmapffval  42700  sticksstones22  42976  sticksstones23  42977  aks6d1c6isolem3  42984  prjspeclsp  43385  sn-isghm  43446  eldiophb  43529  eldioph  43530  diophrw  43531  eldioph2  43534  eldioph2b  43535  eldioph3  43538  diophin  43544  diophun  43545  diophrex  43547  rexrabdioph  43562  rmxypairf1o  43679  hbtlem1  43891  hbtlem7  43893  tfsconcatrn  44110  nzss  45068  dropab1  45197  dropab2  45198  iineq12dv  45865  supsubc  46110  dfaimafn  47943  dfatsnafv2  48030  rnfdmpr  48059  f1oresf1o  48068  imasetpreimafvbijlemfo  48195  fargshiftfo  48232  sprval  48269  sprvalpw  48270  prprval  48304  prprvalpw  48305  prprspr2  48308  isgrim  48688  isgrlim  48788  setrecseq  50504