Theorem abbidv 2800

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1538   = wceq 1540  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723

This theorem is referenced by:  rabbidva2  3433  cdeqab  3766  sbceqbid  3784  csbeq1  3896  csbeq2  3898  csbeq2d  3899  csbprc  4406  sbcel12  4408  sbceqg  4409  csbnestgfw  4419  csbnestgf  4424  pweqALT  4617  sneq  4638  csbsng  4712  unieqOLD  4920  uniprg  4925  csbuni  4940  inteq  4953  iineq1  5014  iineq2  5017  dfiin2g  5035  iinrab  5072  iinxprg  5092  opabbid  5213  opabbidv  5214  axrep6g  5293  imasng  6082  predres  6340  iotaeq  6508  iotabi  6509  dfimafn  6954  fnsnfvOLD  6971  fliftf  7315  oprabbid  7477  oprabbidv  7478  frecseq123  8273  csbfrecsg  8275  wrecseq123OLD  8306  rdglim2  8438  qseq1  8763  qseq2  8764  qsinxp  8793  mapvalg  8836  fsetexb  8864  ixpsnval  8900  ixpeq1  8908  fival  9413  tcvalg  9739  karden  9896  acneq  10044  infmap2  10219  cfval  10248  cflim3  10263  axdclem  10520  axdc  10522  rankcf  10778  genpv  11000  negfi  12170  supadd  12189  hashf1lem2  14424  hashf1  14425  hashfac  14426  csbwrdg  14501  cshimadifsn  14787  cshimadifsn0  14788  cleq1  14937  dfrtrcl2  15016  shftlem  15022  shftfib  15026  vdwlem6  16926  cshwsiun  17040  lubfval  18313  glbfval  18326  eqglact  19102  qus0subgbas  19120  isghm  19137  symgval  19284  sylow1lem2  19515  sylow3lem1  19543  efgval  19633  dmdprd  19916  ixpsnbasval  21066  pzriprnglem10  21350  pzriprnglem11  21351  cssval  21545  aspval2  21762  ressmplbas2  21893  tgval  22778  clsval2  22874  lpfval  22962  lpval  22963  islocfin  23341  ptval  23394  hauspwpwf1  23811  ptcmplem2  23877  snclseqg  23940  ustval  24027  itg2val  25578  limcfval  25721  plyval  26045  addsval  27792  addscom  27796  addsass  27835  mulsval  27922  mulscom  27952  addsdi  27968  mulsass  27979  mulsunif2lem  27982  precsexlemcbv  28017  precsexlem3  28020  elreno  28103  readdscl  28107  remulscl  28110  isismt  28218  nb3grprlem1  29070  vtxdun  29171  rgrx0ndm  29283  ewlksfval  29291  rusgrnumwwlkb0  29658  eclclwwlkn1  29761  avril1  30149  nmoofval  30448  nmooval  30449  nmoo0  30477  nmopval  31542  nmfnval  31562  iunrdx  32228  iinabrex  32233  disjabrex  32246  disjabrexf  32247  dfimafnf  32293  curry2ima  32363  cshwrnid  32558  nsgqusf1olem2  32965  pstmval  33339  pstmfval  33340  sigaval  33573  measval  33660  orvcval  33920  bnj956  34251  bnj18eq1  34402  bnj1318  34500  fnrelpredd  34556  derangval  34622  satfdm  34824  fmlasuc  34841  satffunlem1lem2  34858  satffunlem2lem2  34861  mclsval  35018  dfrdg2  35237  dfrdg3  35238  altxpeq1  35415  altxpeq2  35416  bj-snsetex  36308  bj-sngleq  36312  bj-projeq  36337  bj-projval  36341  bj-imafv  36596  csboprabg  36675  finxpeq1  36731  finxpeq2  36732  csbfinxpg  36733  finxpreclem6  36741  ptrest  36951  poimirlem26  36978  poimirlem27  36979  poimirlem28  36980  mblfinlem3  36991  cnambfre  37000  itg2addnc  37006  areacirclem5  37044  sdclem2  37074  sdc  37076  ismtyval  37132  elghomlem1OLD  37217  iineq12f  37496  eccnvepres  37612  lfl1dim  38455  ldual1dim  38500  glbconxN  38713  lineset  39073  pointsetN  39076  psubspset  39079  pmapglb2xN  39107  polval2N  39241  psubclsetN  39271  lautset  39417  pautsetN  39433  tendofset  40093  tendoset  40094  dva1dim  40320  dia1dim2  40397  dib1dim2  40503  diclspsn  40529  dih1dimatlem  40664  dihglb2  40677  hdmap1ffval  41130  hdmapffval  41161  hgmapffval  41220  sticksstones22  41451  prjspeclsp  41817  eldiophb  41958  eldioph  41959  diophrw  41960  eldioph2  41963  eldioph2b  41964  eldioph3  41967  diophin  41973  diophun  41974  diophrex  41976  rexrabdioph  41995  rmxypairf1o  42113  hbtlem1  42328  hbtlem7  42330  tfsconcatrn  42555  nzss  43539  dropab1  43669  dropab2  43670  supsubc  44522  dfaimafn  46332  dfatsnafv2  46419  rnfdmpr  46448  f1oresf1o  46457  imasetpreimafvbijlemfo  46532  fargshiftfo  46569  sprval  46606  sprvalpw  46607  prprval  46641  prprvalpw  46642  prprspr2  46645  setrecseq  47892