Theorem abbidv 2885

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 1924	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		abbi1 2884	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	2, 3	syl 17	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1531   = wceq 1533  {cab 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814

This theorem is referenced by:  rabbidva2  3477  cdeqab  3761  sbceqbid  3779  csbeq1  3886  csbeq2  3888  csbeq2d  3889  csbprc  4358  sbcel12  4360  sbceqg  4361  csbnestgfw  4371  csbnestgf  4376  pweq  4542  sneq  4571  csbsng  4638  unieq  4840  csbuni  4860  inteq  4872  iineq1  4929  iineq2  4932  dfiin2g  4950  iinrab  4984  iinxprg  5004  opabbid  5124  imasng  5946  iotaeq  6321  iotabi  6322  dfimafn  6723  fnsnfv  6738  fliftf  7062  oprabbid  7213  wrecseq123  7942  rdglim2  8062  qseq1  8337  qseq2  8338  qsinxp  8367  mapvalg  8410  ixpsnval  8458  ixpeq1  8466  fival  8870  tcvalg  9174  karden  9318  acneq  9463  infmap2  9634  cfval  9663  cflim3  9678  axdclem  9935  axdc  9937  rankcf  10193  genpv  10415  negfi  11583  supadd  11603  hashf1lem2  13808  hashf1  13809  hashfac  13810  csbwrdg  13889  cshimadifsn  14185  cshimadifsn0  14186  cleq1  14337  dfrtrcl2  14415  shftlem  14421  shftfib  14425  vdwlem6  16316  cshwsiun  16427  lubfval  17582  glbfval  17595  eqglact  18325  isghm  18352  symgval  18491  sylow1lem2  18718  sylow3lem1  18746  efgval  18837  dmdprd  19114  ixpsnbasval  19976  aspval2  20121  ressmplbas2  20230  cssval  20820  tgval  21557  clsval2  21652  lpfval  21740  lpval  21741  islocfin  22119  ptval  22172  hauspwpwf1  22589  ptcmplem2  22655  snclseqg  22718  ustval  22805  itg2val  24323  limcfval  24464  plyval  24777  isismt  26314  nb3grprlem1  27156  vtxdun  27257  rgrx0ndm  27369  ewlksfval  27377  wwlksnfiOLD  27679  rusgrnumwwlkb0  27744  eclclwwlkn1  27848  avril1  28236  nmoofval  28533  nmooval  28534  nmoo0  28562  nmopval  29627  nmfnval  29647  iunrdx  30309  disjabrex  30326  disjabrexf  30327  dfimafnf  30375  curry2ima  30438  cshwrnid  30630  pstmval  31130  pstmfval  31131  sigaval  31365  measval  31452  orvcval  31710  bnj956  32043  bnj18eq1  32194  bnj1318  32292  derangval  32409  satfdm  32611  fmlasuc  32628  satffunlem1lem2  32645  satffunlem2lem2  32648  mclsval  32805  dfrdg2  33035  dfrdg3  33036  frecseq123  33114  altxpeq1  33429  altxpeq2  33430  bj-snsetex  34270  bj-sngleq  34274  bj-projeq  34299  bj-projval  34303  bj-imafv  34527  csbwrecsg  34602  csboprabg  34605  finxpeq1  34661  finxpeq2  34662  csbfinxpg  34663  finxpreclem6  34671  ptrest  34885  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  mblfinlem3  34925  cnambfre  34934  itg2addnc  34940  areacirclem5  34980  sdclem2  35011  sdc  35013  ismtyval  35072  elghomlem1OLD  35157  iineq12f  35436  eccnvepres  35531  lfl1dim  36251  ldual1dim  36296  glbconxN  36508  lineset  36868  pointsetN  36871  psubspset  36874  pmapglb2xN  36902  polval2N  37036  psubclsetN  37066  lautset  37212  pautsetN  37228  tendofset  37888  tendoset  37889  dva1dim  38115  dia1dim2  38192  dib1dim2  38298  diclspsn  38324  dih1dimatlem  38459  dihglb2  38472  hdmap1ffval  38925  hdmapffval  38956  hgmapffval  39015  prjspeclsp  39255  eldiophb  39347  eldioph  39348  diophrw  39349  eldioph2  39352  eldioph2b  39353  eldioph3  39356  diophin  39362  diophun  39363  diophrex  39365  rexrabdioph  39384  rmxypairf1o  39501  hbtlem1  39716  hbtlem7  39718  nzss  40642  dropab1  40772  dropab2  40773  supsubc  41613  dfaimafn  43357  dfatsnafv2  43444  rnfdmpr  43473  f1oresf1o  43482  imasetpreimafvbijlemfo  43558  fargshiftfo  43595  sprval  43634  sprvalpw  43635  prprval  43669  prprvalpw  43670  prprspr2  43673  setrecseq  44781