Theorem rabbidva 3422

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 579	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rabbidva2 3417	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-rab 3416

This theorem is referenced by:  rabbidv  3423  rabeqbidva  3432  rabeqbidvaOLD  3433  rabbi2dva  4201  rabxfrd  5387  seinxp  5738  ordintdif  6403  f1oresrab  7116  onsucmin  7813  suppval1  8163  mptsuppd  8184  naddasslem1  8704  naddasslem2  8705  naddsuc2  8711  cantnflem1  9701  harsucnn  10010  dfinfre  12221  ixxin  13377  mptnn0fsuppr  14015  scshwfzeqfzo  14843  incexc2  15852  smueqlem  16507  gcdass  16564  lcmass  16631  pcneg  16892  ramval  17026  acsfn  17669  monpropd  17748  f1omvdcnv  19423  pmtrmvd  19435  submod  19548  odngen  19556  sylow3lem6  19611  efgsfo  19718  rrgsupp  20659  acsfn1p  20757  rngqiprngimf1  21259  dsmmbas2  21695  dsmmacl  21699  frlmbas  21713  frlmsslss2  21733  mplsubglem2  21959  ltbwe  22000  coe1mul2lem2  22203  scmatmats  22447  mretopd  23028  ordtbaslem  23124  ordtrest  23138  ordtrest2lem  23139  leordtval  23149  xkopt  23591  xkoco1cn  23593  xkoco2cn  23594  xkoinjcn  23623  r0cld  23674  utopsnneiplem  24184  stdbdbl  24454  minveclem3b  25378  minveclem4  25382  lhop1lem  25968  idomrootle  26128  mumul  27141  sqff1o  27142  lgsquadlem1  27341  lgsquadlem2  27342  2lgslem1a  27352  lrrecse  27892  lrrecpred  27894  elntg2  28910  edglnl  29068  nbupgr  29269  vtxdun  29407  wwlksnextprop  29840  wpthswwlks2on  29889  rusgrnumwwlkslem  29897  rusgrnumwwlks  29902  clwlknf1oclwwlkn  30011  frcond3  30196  extwwlkfab  30279  grpoidinv2  30442  grpoinv  30452  xppreima  32569  qusker  33310  nsgqusf1olem3  33376  fedgmullem2  33616  ply1annidllem  33681  zarclsun  33847  cnvordtrestixx  33890  ordtrestNEW  33898  ordtrest2NEWlem  33899  fnrelpredd  35066  satfv1lem  35330  satefvfmla0  35386  satefvfmla1  35393  lineunray  36111  lineelsb2  36112  linecom  36114  ee7.2aOLD  36425  poimirlem26  37616  poimirlem27  37617  mbfposadd  37637  cnambfre  37638  itg2addnclem2  37642  iblabsnclem  37653  ftc1anclem1  37663  lfl1dim2N  39086  pmapat  39728  pmapglbx  39734  dvhb1dimN  40951  dia0  41017  mapdval2N  41595  mapdsn  41606  hlhilocv  41922  isprimroot  42052  aks6d1c6isolem3  42135  unitscyglem5  42158  istopclsd  42670  diophren  42783  rabrenfdioph  42784  pwfi2f1o  43067  idomodle  43162  hausgraph  43176  nadd1rabtr  43359  nadd1rabex  43361  nadd1suc  43363  minregex2  43506  fsovcnvlem  43984  ntrneifv3  44053  ntrneifv4  44056  clsneifv3  44081  clsneifv4  44082  neicvgfv  44092  nzss  44289  preimaiocmnf  45537  preimaicomnf  46688  smfsupxr  46793  smfliminflem  46807  sprvalpwle2  47451  fpprmod  47689  dfsclnbgr2  47807  dfvopnbgr2  47814  uspgrlimlem2  47949  rmsupp0  48291  lco0  48351  rrxlinesc  48663  rrxlinec  48664  rrx2line  48668  rrx2vlinest  48669  rrx2linest  48670  rrx2linesl  48671  rrx2linest2  48672  2sphere  48677  2sphere0  48678  line2  48680  itsclinecirc0b  48702