Theorem abbidv 2829

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 1957	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		abbi 2828	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	2, 3	syl 18	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755

This theorem is referenced by:  rabbidva2  3418  cdeqab  3734  sbceqbid  3752  csbeq1  3857  csbeq2  3859  csbeq2d  3860  csbeq2dv  3861  csbprc  4375  sbcel12  4377  sbceqg  4378  csbnestgfw  4388  csbnestgf  4393  pweqALT  4578  sneq  4600  csbsng  4675  uniprg  4889  csbuni  4904  inteq  4916  iineq1  4975  iineq2  4978  iuneq12d  4987  dfiin2g  4996  iinrab  5034  iinxprg  5056  opabbid  5177  opabbidv  5178  axrep6g  5252  imasng  6088  predres  6342  iotaeq  6506  iotabi  6507  dfimafn  6945  fliftf  7315  oprabbid  7477  oprabbidv  7478  frecseq123  8280  csbfrecsg  8282  rdglim2  8420  qseq1  8755  qseq2  8756  snecg  8776  qsinxp  8792  mapvalg  8834  fsetexb  8862  ixpsnval  8899  ixpeq1  8907  fival  9373  tcvalg  9706  karden  9882  acneq  10028  infmap2  10201  cfval  10231  cflim3  10247  axdclem  10504  axdc  10506  rankcf  10763  genpv  10985  negfi  12165  supadd  12184  hashf1lem2  14495  hashf1  14496  hashfac  14497  csbwrdg  14583  cshimadifsn  14868  cshimadifsn0  14869  cleq1  15022  dfrtrcl2  15101  shftlem  15107  shftfib  15111  vdwlem6  17047  cshwsiun  17160  lubfval  18405  glbfval  18418  eqglact  19248  qus0subgbas  19270  isghm  19287  symgval  19442  sylow1lem2  19670  sylow3lem1  19698  efgval  19788  dmdprd  20071  ixpsnbasval  21310  pzriprnglem10  21621  pzriprnglem11  21622  cssval  21813  aspval2  22029  ressmplbas2  22158  tgval  23093  clsval2  23188  lpfval  23276  lpval  23277  islocfin  23655  ptval  23708  hauspwpwf1  24125  ptcmplem2  24191  snclseqg  24254  ustval  24341  itg2val  25868  limcfval  26012  plyval  26331  addsval  28136  addscom  28140  addsass  28179  addbday  28192  mulsval  28283  mulscom  28313  addsdi  28329  mulsass  28340  mulsunif2lem  28343  precsexlemcbv  28380  precsexlem3  28383  halfcut  28632  pw2cut2  28636  elreno  28665  readdscl  28673  remulscl  28676  isismt  28784  nb3grprlem1  29711  vtxdun  29812  rgrx0ndm  29924  ewlksfval  29932  rusgrnumwwlkb0  30304  eclclwwlkn1  30407  avril1  30795  nmoofval  31095  nmooval  31096  nmoo0  31124  nmopval  32189  nmfnval  32209  iunrdx  32889  iinabrex  32895  disjabrex  32908  disjabrexf  32909  dfimafnf  32962  curry2ima  33035  cshwrnid  33262  nsgqusf1olem2  33704  pstmval  34266  pstmfval  34267  sigaval  34482  measval  34569  orvcval  34829  bnj956  35146  bnj18eq1  35296  bnj1318  35394  fnrelpredd  35463  kardval  35546  kard0  35548  derangval  35640  satfdm  35842  fmlasuc  35859  satffunlem1lem2  35876  satffunlem2lem2  35879  mclsval  36036  dfrdg2  36266  dfrdg3  36267  altxpeq1  36446  altxpeq2  36447  ixpeq12dv  36709  cbvcsbdavw  36752  cbvcsbdavw2  36753  cbviundavw  36755  cbviindavw  36756  cbvopab1davw  36757  cbvopab2davw  36758  cbvopabdavw  36759  cbviotadavw  36762  cbvoprab1davw  36764  cbvoprab2davw  36765  cbvoprab3davw  36766  cbvoprab123davw  36767  cbvoprab12davw  36768  cbvoprab23davw  36769  cbvoprab13davw  36770  cbvixpdavw  36771  cbviundavw2  36779  cbviindavw2  36780  cbvixpdavw2  36787  bj-snsetex  37580  bj-sngleq  37584  bj-projeq  37609  bj-projval  37613  bj-imafv  37876  csboprabg  37957  finxpeq1  38013  finxpeq2  38014  csbfinxpg  38015  finxpreclem6  38023  ptrest  38251  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  mblfinlem3  38291  cnambfre  38300  itg2addnc  38306  areacirclem5  38344  sdclem2  38374  sdc  38376  ismtyval  38432  elghomlem1OLD  38517  iineq12f  38794  eccnvepres  38916  ecqmap  39079  lfl1dim  39876  ldual1dim  39921  glbconxN  40133  lineset  40493  pointsetN  40496  psubspset  40499  pmapglb2xN  40527  polval2N  40661  psubclsetN  40691  lautset  40837  pautsetN  40853  tendofset  41513  tendoset  41514  dva1dim  41740  dia1dim2  41817  dib1dim2  41923  diclspsn  41949  dih1dimatlem  42084  dihglb2  42097  hdmap1ffval  42550  hdmapffval  42581  hgmapffval  42640  sticksstones22  42916  sticksstones23  42917  aks6d1c6isolem3  42924  prjspeclsp  43327  sn-isghm  43388  eldiophb  43471  eldioph  43472  diophrw  43473  eldioph2  43476  eldioph2b  43477  eldioph3  43480  diophin  43486  diophun  43487  diophrex  43489  rexrabdioph  43504  rmxypairf1o  43621  hbtlem1  43833  hbtlem7  43835  tfsconcatrn  44052  nzss  45010  dropab1  45139  dropab2  45140  iineq12dv  45807  supsubc  46052  dfaimafn  47885  dfatsnafv2  47972  rnfdmpr  48001  f1oresf1o  48010  imasetpreimafvbijlemfo  48137  fargshiftfo  48174  sprval  48211  sprvalpw  48212  prprval  48246  prprvalpw  48247  prprspr2  48250  isgrim  48630  isgrlim  48730  setrecseq  50446