Theorem rabbidva 3429

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rab 3424

This theorem is referenced by:  rabbidv  3430  rabeqbidva  3439  rabeqbidvaOLD  3440  rabbi2dva  4186  rabxfrd  5389  seinxp  5746  ordintdif  6413  f1oresrab  7124  onsucmin  7816  suppval1  8161  mptsuppd  8182  naddasslem1  8680  naddasslem2  8681  naddsuc2  8687  cantnflem1  9657  harsucnn  9983  dfinfre  12195  ixxin  13388  mptnn0fsuppr  14034  scshwfzeqfzo  14862  incexc2  15891  smueqlem  16547  gcdass  16604  lcmass  16671  pcneg  16933  ramval  17067  acsfn  17714  monpropd  17793  f1omvdcnv  19513  pmtrmvd  19525  submod  19638  odngen  19646  sylow3lem6  19701  efgsfo  19808  rrgsupp  20785  acsfn1p  20879  rngqiprngimf1  21410  dsmmbas2  21855  dsmmacl  21859  frlmbas  21873  frlmsslss2  21893  mplsubglem2  22118  ltbwe  22163  coe1mul2lem2  22397  scmatmats  22636  mretopd  23217  ordtbaslem  23313  ordtrest  23327  ordtrest2lem  23328  leordtval  23338  xkopt  23780  xkoco1cn  23782  xkoco2cn  23783  xkoinjcn  23812  r0cld  23863  utopsnneiplem  24372  stdbdbl  24642  minveclem3b  25555  minveclem4  25559  lhop1lem  26140  idomrootle  26298  mumul  27310  sqff1o  27311  lgsquadlem1  27509  lgsquadlem2  27510  2lgslem1a  27520  lrrecse  28100  lrrecpred  28102  plngcplem  29024  elntg2  29275  edglnl  29433  nbupgr  29634  vtxdun  29771  wwlksnextprop  30201  wpthswwlks2on  30253  rusgrnumwwlkslem  30261  rusgrnumwwlks  30266  clwlknf1oclwwlkn  30375  frcond3  30560  extwwlkfab  30643  grpoidinv2  30807  grpoinv  30817  xppreima  32930  qusker  33611  nsgqusf1olem3  33667  fedgmullem2  33964  ply1annidllem  34035  zarclsun  34204  cnvordtrestixx  34247  ordtrestNEW  34255  ordtrest2NEWlem  34256  fnrelpredd  35424  fineqvnttrclse  35459  satfv1lem  35752  satefvfmla0  35808  satefvfmla1  35815  lineunray  36537  lineelsb2  36538  linecom  36540  ee7.2aOLD  36860  poimirlem26  38184  poimirlem27  38185  mbfposadd  38205  cnambfre  38206  itg2addnclem2  38210  iblabsnclem  38221  ftc1anclem1  38231  lfl1dim2N  39785  pmapat  40426  pmapglbx  40432  dvhb1dimN  41649  dia0  41715  mapdval2N  42293  mapdsn  42304  hlhilocv  42620  isprimroot  42749  aks6d1c6isolem3  42832  unitscyglem5  42855  istopclsd  43322  diophren  43431  rabrenfdioph  43432  pwfi2f1o  43714  idomodle  43809  hausgraph  43823  nadd1rabtr  44006  nadd1rabex  44008  nadd1suc  44010  minregex2  44152  fsovcnvlem  44630  ntrneifv3  44699  ntrneifv4  44702  clsneifv3  44727  clsneifv4  44728  neicvgfv  44738  nzss  44918  preimaiocmnf  46167  preimaicomnf  47316  smfsupxr  47421  smfliminflem  47435  sprvalpwle2  48126  fpprmod  48380  dfsclnbgr2  48499  dfvopnbgr2  48506  uspgrlimlem2  48642  rmsupp0  49032  lco0  49091  rrxlinesc  49399  rrxlinec  49400  rrx2line  49404  rrx2vlinest  49405  rrx2linest  49406  rrx2linesl  49407  rrx2linest2  49408  2sphere  49413  2sphere0  49414  line2  49416  itsclinecirc0b  49438