Theorem abbidv 2808

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  {cab 2716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731

This theorem is referenced by:  rabbidva2  3412  cdeqab  3706  sbceqbid  3724  csbeq1  3836  csbeq2  3838  csbeq2d  3839  csbprc  4341  sbcel12  4343  sbceqg  4344  csbnestgfw  4354  csbnestgf  4359  pweqALT  4551  sneq  4572  csbsng  4645  unieqOLD  4852  uniprg  4857  csbuni  4871  inteq  4883  iineq1  4942  iineq2  4945  dfiin2g  4963  iinrab  4999  iinxprg  5019  opabbid  5140  opabbidv  5141  axrep6g  5218  imasng  5994  predres  6246  iotaeq  6408  iotabi  6409  dfimafn  6841  fnsnfvOLD  6857  fliftf  7195  oprabbid  7349  oprabbidv  7350  frecseq123  8107  csbfrecsg  8109  wrecseq123OLD  8140  rdglim2  8272  qseq1  8561  qseq2  8562  qsinxp  8591  mapvalg  8634  fsetexb  8661  ixpsnval  8697  ixpeq1  8705  fival  9180  tcvalg  9505  karden  9662  acneq  9808  infmap2  9983  cfval  10012  cflim3  10027  axdclem  10284  axdc  10286  rankcf  10542  genpv  10764  negfi  11933  supadd  11952  hashf1lem2  14179  hashf1  14180  hashfac  14181  csbwrdg  14256  cshimadifsn  14551  cshimadifsn0  14552  cleq1  14703  dfrtrcl2  14782  shftlem  14788  shftfib  14792  vdwlem6  16696  cshwsiun  16810  lubfval  18077  glbfval  18090  eqglact  18816  isghm  18843  symgval  18985  sylow1lem2  19213  sylow3lem1  19241  efgval  19332  dmdprd  19610  ixpsnbasval  20489  cssval  20896  aspval2  21111  ressmplbas2  21237  tgval  22114  clsval2  22210  lpfval  22298  lpval  22299  islocfin  22677  ptval  22730  hauspwpwf1  23147  ptcmplem2  23213  snclseqg  23276  ustval  23363  itg2val  24902  limcfval  25045  plyval  25363  isismt  26904  nb3grprlem1  27756  vtxdun  27857  rgrx0ndm  27969  ewlksfval  27977  rusgrnumwwlkb0  28345  eclclwwlkn1  28448  avril1  28836  nmoofval  29133  nmooval  29134  nmoo0  29162  nmopval  30227  nmfnval  30247  iunrdx  30912  iinabrex  30917  disjabrex  30930  disjabrexf  30931  dfimafnf  30980  curry2ima  31050  cshwrnid  31242  nsgqusf1olem2  31608  pstmval  31854  pstmfval  31855  sigaval  32088  measval  32175  orvcval  32433  bnj956  32765  bnj18eq1  32916  bnj1318  33014  fnrelpredd  33070  derangval  33138  satfdm  33340  fmlasuc  33357  satffunlem1lem2  33374  satffunlem2lem2  33377  mclsval  33534  dfrdg2  33780  dfrdg3  33781  addsval  34135  addscom  34138  altxpeq1  34284  altxpeq2  34285  bj-snsetex  35162  bj-sngleq  35166  bj-projeq  35191  bj-projval  35195  bj-imafv  35431  csboprabg  35510  finxpeq1  35566  finxpeq2  35567  csbfinxpg  35568  finxpreclem6  35576  ptrest  35785  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  mblfinlem3  35825  cnambfre  35834  itg2addnc  35840  areacirclem5  35878  sdclem2  35909  sdc  35911  ismtyval  35967  elghomlem1OLD  36052  iineq12f  36331  eccnvepres  36423  lfl1dim  37142  ldual1dim  37187  glbconxN  37399  lineset  37759  pointsetN  37762  psubspset  37765  pmapglb2xN  37793  polval2N  37927  psubclsetN  37957  lautset  38103  pautsetN  38119  tendofset  38779  tendoset  38780  dva1dim  39006  dia1dim2  39083  dib1dim2  39189  diclspsn  39215  dih1dimatlem  39350  dihglb2  39363  hdmap1ffval  39816  hdmapffval  39847  hgmapffval  39906  sticksstones22  40131  prjspeclsp  40458  eldiophb  40586  eldioph  40587  diophrw  40588  eldioph2  40591  eldioph2b  40592  eldioph3  40595  diophin  40601  diophun  40602  diophrex  40604  rexrabdioph  40623  rmxypairf1o  40740  hbtlem1  40955  hbtlem7  40957  nzss  41942  dropab1  42072  dropab2  42073  supsubc  42899  dfaimafn  44668  dfatsnafv2  44755  rnfdmpr  44784  f1oresf1o  44793  imasetpreimafvbijlemfo  44868  fargshiftfo  44905  sprval  44942  sprvalpw  44943  prprval  44977  prprvalpw  44978  prprspr2  44981  setrecseq  46402