Theorem rabbidva 3401

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

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3395

This theorem is referenced by:  rabbidv  3402  rabeqbidva  3411  rabeqbidvaOLD  3412  rabbi2dva  4177  rabxfrd  5356  seinxp  5703  ordintdif  6358  f1oresrab  7061  onsucmin  7754  suppval1  8099  mptsuppd  8120  naddasslem1  8612  naddasslem2  8613  naddsuc2  8619  cantnflem1  9585  harsucnn  9894  dfinfre  12106  ixxin  13265  mptnn0fsuppr  13906  scshwfzeqfzo  14733  incexc2  15745  smueqlem  16401  gcdass  16458  lcmass  16525  pcneg  16786  ramval  16920  acsfn  17565  monpropd  17644  f1omvdcnv  19323  pmtrmvd  19335  submod  19448  odngen  19456  sylow3lem6  19511  efgsfo  19618  rrgsupp  20586  acsfn1p  20684  rngqiprngimf1  21207  dsmmbas2  21644  dsmmacl  21648  frlmbas  21662  frlmsslss2  21682  mplsubglem2  21908  ltbwe  21949  coe1mul2lem2  22152  scmatmats  22396  mretopd  22977  ordtbaslem  23073  ordtrest  23087  ordtrest2lem  23088  leordtval  23098  xkopt  23540  xkoco1cn  23542  xkoco2cn  23543  xkoinjcn  23572  r0cld  23623  utopsnneiplem  24133  stdbdbl  24403  minveclem3b  25326  minveclem4  25330  lhop1lem  25916  idomrootle  26076  mumul  27089  sqff1o  27090  lgsquadlem1  27289  lgsquadlem2  27290  2lgslem1a  27300  lrrecse  27854  lrrecpred  27856  elntg2  28930  edglnl  29088  nbupgr  29289  vtxdun  29427  wwlksnextprop  29857  wpthswwlks2on  29906  rusgrnumwwlkslem  29914  rusgrnumwwlks  29919  clwlknf1oclwwlkn  30028  frcond3  30213  extwwlkfab  30296  grpoidinv2  30459  grpoinv  30469  xppreima  32588  qusker  33286  nsgqusf1olem3  33352  fedgmullem2  33597  ply1annidllem  33668  zarclsun  33837  cnvordtrestixx  33880  ordtrestNEW  33888  ordtrest2NEWlem  33889  fnrelpredd  35056  fineqvnttrclse  35077  satfv1lem  35339  satefvfmla0  35395  satefvfmla1  35402  lineunray  36125  lineelsb2  36126  linecom  36128  ee7.2aOLD  36439  poimirlem26  37630  poimirlem27  37631  mbfposadd  37651  cnambfre  37652  itg2addnclem2  37656  iblabsnclem  37667  ftc1anclem1  37677  lfl1dim2N  39105  pmapat  39746  pmapglbx  39752  dvhb1dimN  40969  dia0  41035  mapdval2N  41613  mapdsn  41624  hlhilocv  41940  isprimroot  42070  aks6d1c6isolem3  42153  unitscyglem5  42176  istopclsd  42677  diophren  42790  rabrenfdioph  42791  pwfi2f1o  43073  idomodle  43168  hausgraph  43182  nadd1rabtr  43365  nadd1rabex  43367  nadd1suc  43369  minregex2  43512  fsovcnvlem  43990  ntrneifv3  44059  ntrneifv4  44062  clsneifv3  44087  clsneifv4  44088  neicvgfv  44098  nzss  44294  preimaiocmnf  45545  preimaicomnf  46696  smfsupxr  46801  smfliminflem  46815  sprvalpwle2  47477  fpprmod  47715  dfsclnbgr2  47834  dfvopnbgr2  47841  uspgrlimlem2  47977  rmsupp0  48356  lco0  48416  rrxlinesc  48724  rrxlinec  48725  rrx2line  48729  rrx2vlinest  48730  rrx2linest  48731  rrx2linesl  48732  rrx2linest2  48733  2sphere  48738  2sphere0  48739  line2  48741  itsclinecirc0b  48763