Theorem rabbidva 3424

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) (Proof shortened by SN, 3-Dec-2023.)

Hypothesis

Ref	Expression
rabbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabbidva	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidva

Step	Hyp	Ref	Expression
1		rabbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 590	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rabbidva2 3420	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {crab 3418

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 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-rab 3419

This theorem is used by:  rabbidv  3425  rabeqbidva  3434  rabeqbidvaOLD  3435  rabbi2dva  4178  rabxfrd  5390  seinxp  5747  ordintdif  6416  f1oresrab  7127  onsucmin  7823  suppval1  8168  mptsuppd  8189  naddasslem1  8687  naddasslem2  8688  naddsuc2  8694  cantnflem1  9665  harsucnn  10000  dfinfre  12211  ixxin  13405  mptnn0fsuppr  14053  scshwfzeqfzo  14887  incexc2  15915  smueqlem  16570  gcdass  16627  lcmass  16694  pcneg  16956  ramval  17090  acsfn  17737  monpropd  17816  f1omvdcnv  19558  pmtrmvd  19570  submod  19683  odngen  19691  sylow3lem6  19746  efgsfo  19853  rrgsupp  20850  acsfn1p  20952  rngqiprngimf1  21490  dsmmbas2  21937  dsmmacl  21941  frlmbas  21955  frlmsslss2  21975  mplsubglem2  22200  ltbwe  22245  coe1mul2lem2  22479  scmatmats  22718  mretopd  23299  ordtbaslem  23395  ordtrest  23409  ordtrest2lem  23410  leordtval  23420  xkopt  23863  xkoco1cn  23865  xkoco2cn  23866  xkoinjcn  23895  r0cld  23946  utopsnneiplem  24455  stdbdbl  24725  minveclem3b  25638  minveclem4  25642  lhop1lem  26223  idomrootle  26381  mumul  27396  sqff1o  27397  lgsquadlem1  27595  lgsquadlem2  27596  2lgslem1a  27606  lrrecse  28186  lrrecpred  28188  plngcplem  29118  elntg2  29390  edglnl  29548  nbupgr  29752  vtxdun  29889  wwlksnextprop  30328  wpthswwlks2on  30380  rusgrnumwwlkslem  30388  rusgrnumwwlks  30393  clwlknf1oclwwlkn  30502  frcond3  30691  extwwlkfab  30774  grpoidinv2  30938  grpoinv  30948  xppreima  33061  qusker  33733  nsgqusf1olem3  33788  fedgmullem2  34084  ply1annidllem  34155  zarclsun  34324  cnvordtrestixx  34367  ordtrestNEW  34375  ordtrest2NEWlem  34376  fnrelpredd  35540  fineqvnttrclse  35594  satfv1lem  35891  satefvfmla0  35947  satefvfmla1  35954  lineunray  36676  lineelsb2  36677  linecom  36679  nmulrid  36726  ee7.2aOLD  37029  poimirlem26  38354  poimirlem27  38355  mbfposadd  38375  cnambfre  38376  itg2addnclem2  38380  iblabsnclem  38391  ftc1anclem1  38401  lfl1dim2N  39954  pmapat  40595  pmapglbx  40601  dvhb1dimN  41818  dia0  41884  mapdval2N  42462  mapdsn  42473  hlhilocv  42789  isprimroot  42918  aks6d1c6isolem3  43001  unitscyglem5  43024  istopclsd  43489  diophren  43598  rabrenfdioph  43599  pwfi2f1o  43881  idomodle  43976  hausgraph  43990  nadd1rabtr  44173  nadd1rabex  44175  nadd1suc  44177  minregex2  44319  fsovcnvlem  44797  ntrneifv3  44866  ntrneifv4  44869  clsneifv3  44894  clsneifv4  44895  neicvgfv  44905  nzss  45085  preimaiocmnf  46334  preimaicomnf  47483  smfsupxr  47588  smfliminflem  47602  sprvalpwle2  48296  fpprmod  48550  dfsclnbgr2  48669  dfvopnbgr2  48676  uspgrlimlem2  48812  rmsupp0  49205  lco0  49264  rrxlinesc  49572  rrxlinec  49573  rrx2line  49577  rrx2vlinest  49578  rrx2linest  49579  rrx2linesl  49580  rrx2linest2  49581  2sphere  49586  2sphere0  49587  line2  49589  itsclinecirc0b  49611