Theorem rabbidva 3426

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 3421	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  {crab 3419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-rab 3420

This theorem is referenced by:  rabbidv  3427  rabeqbidva  3436  rabeqbidvaOLD  3437  rabbi2dva  4206  rabxfrd  5397  seinxp  5749  ordintdif  6414  f1oresrab  7127  onsucmin  7823  suppval1  8173  mptsuppd  8194  naddasslem1  8714  naddasslem2  8715  naddsuc2  8721  cantnflem1  9711  harsucnn  10020  dfinfre  12231  ixxin  13386  mptnn0fsuppr  14022  scshwfzeqfzo  14847  incexc2  15856  smueqlem  16509  gcdass  16566  lcmass  16633  pcneg  16894  ramval  17028  acsfn  17673  monpropd  17752  f1omvdcnv  19430  pmtrmvd  19442  submod  19555  odngen  19563  sylow3lem6  19618  efgsfo  19725  rrgsupp  20669  acsfn1p  20768  rngqiprngimf1  21272  dsmmbas2  21711  dsmmacl  21715  frlmbas  21729  frlmsslss2  21749  mplsubglem2  21975  ltbwe  22016  coe1mul2lem2  22219  scmatmats  22465  mretopd  23046  ordtbaslem  23142  ordtrest  23156  ordtrest2lem  23157  leordtval  23167  xkopt  23609  xkoco1cn  23611  xkoco2cn  23612  xkoinjcn  23641  r0cld  23692  utopsnneiplem  24202  stdbdbl  24474  minveclem3b  25398  minveclem4  25402  lhop1lem  25988  idomrootle  26148  mumul  27160  sqff1o  27161  lgsquadlem1  27360  lgsquadlem2  27361  2lgslem1a  27371  lrrecse  27911  lrrecpred  27913  elntg2  28930  edglnl  29088  nbupgr  29289  vtxdun  29427  wwlksnextprop  29860  wpthswwlks2on  29909  rusgrnumwwlkslem  29917  rusgrnumwwlks  29922  clwlknf1oclwwlkn  30031  frcond3  30216  extwwlkfab  30299  grpoidinv2  30462  grpoinv  30472  xppreima  32590  qusker  33312  nsgqusf1olem3  33378  fedgmullem2  33616  ply1annidllem  33681  zarclsun  33828  cnvordtrestixx  33871  ordtrestNEW  33879  ordtrest2NEWlem  33880  fnrelpredd  35062  satfv1lem  35326  satefvfmla0  35382  satefvfmla1  35389  lineunray  36107  lineelsb2  36108  linecom  36110  ee7.2aOLD  36421  poimirlem26  37612  poimirlem27  37613  mbfposadd  37633  cnambfre  37634  itg2addnclem2  37638  iblabsnclem  37649  ftc1anclem1  37659  lfl1dim2N  39082  pmapat  39724  pmapglbx  39730  dvhb1dimN  40947  dia0  41013  mapdval2N  41591  mapdsn  41602  hlhilocv  41922  isprimroot  42053  aks6d1c6isolem3  42136  unitscyglem5  42159  istopclsd  42674  diophren  42787  rabrenfdioph  42788  pwfi2f1o  43071  idomodle  43166  hausgraph  43180  nadd1rabtr  43363  nadd1rabex  43365  nadd1suc  43367  minregex2  43510  fsovcnvlem  43988  ntrneifv3  44057  ntrneifv4  44060  clsneifv3  44085  clsneifv4  44086  neicvgfv  44096  nzss  44293  preimaiocmnf  45531  preimaicomnf  46683  smfsupxr  46788  smfliminflem  46802  sprvalpwle2  47434  fpprmod  47672  dfsclnbgr2  47790  dfvopnbgr2  47797  uspgrlimlem2  47914  rmsupp0  48242  lco0  48302  rrxlinesc  48614  rrxlinec  48615  rrx2line  48619  rrx2vlinest  48620  rrx2linest  48621  rrx2linesl  48622  rrx2linest2  48623  2sphere  48628  2sphere0  48629  line2  48631  itsclinecirc0b  48653