Theorem rabbidva 3397

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-rab 3392

This theorem is referenced by:  rabbidv  3398  rabeqbidva  3407  rabeqbidvaOLD  3408  rabbi2dva  4154  rabxfrd  5346  seinxp  5702  ordintdif  6361  f1oresrab  7069  onsucmin  7761  suppval1  8106  mptsuppd  8127  naddasslem1  8620  naddasslem2  8621  naddsuc2  8627  cantnflem1  9601  harsucnn  9913  dfinfre  12128  ixxin  13306  mptnn0fsuppr  13952  scshwfzeqfzo  14779  incexc2  15794  smueqlem  16450  gcdass  16507  lcmass  16574  pcneg  16836  ramval  16970  acsfn  17616  monpropd  17695  f1omvdcnv  19410  pmtrmvd  19422  submod  19535  odngen  19543  sylow3lem6  19598  efgsfo  19705  rrgsupp  20673  acsfn1p  20771  rngqiprngimf1  21293  dsmmbas2  21712  dsmmacl  21716  frlmbas  21730  frlmsslss2  21750  mplsubglem2  21975  ltbwe  22020  coe1mul2lem2  22254  scmatmats  22494  mretopd  23075  ordtbaslem  23171  ordtrest  23185  ordtrest2lem  23186  leordtval  23196  xkopt  23638  xkoco1cn  23640  xkoco2cn  23641  xkoinjcn  23670  r0cld  23721  utopsnneiplem  24230  stdbdbl  24500  minveclem3b  25413  minveclem4  25417  lhop1lem  25998  idomrootle  26156  mumul  27162  sqff1o  27163  lgsquadlem1  27361  lgsquadlem2  27362  2lgslem1a  27372  lrrecse  27952  lrrecpred  27954  elntg2  29072  edglnl  29230  nbupgr  29431  vtxdun  29568  wwlksnextprop  29998  wpthswwlks2on  30050  rusgrnumwwlkslem  30058  rusgrnumwwlks  30063  clwlknf1oclwwlkn  30172  frcond3  30357  extwwlkfab  30440  grpoidinv2  30604  grpoinv  30614  xppreima  32737  qusker  33432  nsgqusf1olem3  33498  fedgmullem2  33814  ply1annidllem  33885  zarclsun  34054  cnvordtrestixx  34097  ordtrestNEW  34105  ordtrest2NEWlem  34106  fnrelpredd  35272  fineqvnttrclse  35305  satfv1lem  35590  satefvfmla0  35646  satefvfmla1  35653  lineunray  36375  lineelsb2  36376  linecom  36378  ee7.2aOLD  36689  poimirlem26  38013  poimirlem27  38014  mbfposadd  38034  cnambfre  38035  itg2addnclem2  38039  iblabsnclem  38050  ftc1anclem1  38060  lfl1dim2N  39614  pmapat  40255  pmapglbx  40261  dvhb1dimN  41478  dia0  41544  mapdval2N  42122  mapdsn  42133  hlhilocv  42449  isprimroot  42578  aks6d1c6isolem3  42661  unitscyglem5  42684  istopclsd  43149  diophren  43258  rabrenfdioph  43259  pwfi2f1o  43541  idomodle  43636  hausgraph  43650  nadd1rabtr  43833  nadd1rabex  43835  nadd1suc  43837  minregex2  43979  fsovcnvlem  44457  ntrneifv3  44526  ntrneifv4  44529  clsneifv3  44554  clsneifv4  44555  neicvgfv  44565  nzss  44761  preimaiocmnf  46005  preimaicomnf  47154  smfsupxr  47259  smfliminflem  47273  sprvalpwle2  47964  fpprmod  48218  dfsclnbgr2  48337  dfvopnbgr2  48344  uspgrlimlem2  48480  rmsupp0  48859  lco0  48918  rrxlinesc  49226  rrxlinec  49227  rrx2line  49231  rrx2vlinest  49232  rrx2linest  49233  rrx2linesl  49234  rrx2linest2  49235  2sphere  49240  2sphere0  49241  line2  49243  itsclinecirc0b  49265