Theorem rabbidva 3418

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-rab 3413

This theorem is used by:  rabbidv  3419  rabeqbidva  3428  rabbi2dva  4171  rabxfrd  5382  seinxp  5739  ordintdif  6409  f1oresrab  7121  onsucmin  7817  suppval1  8164  mptsuppd  8185  naddasslem1  8683  naddasslem2  8684  naddsuc2  8690  cantnflem1  9668  harsucnn  10003  dfinfre  12220  ixxin  13415  mptnn0fsuppr  14063  scshwfzeqfzo  14897  incexc2  15927  smueqlem  16580  gcdass  16637  lcmass  16704  pcneg  16966  ramval  17100  acsfn  17747  monpropd  17826  f1omvdcnv  19571  pmtrmvd  19583  submod  19696  odngen  19704  sylow3lem6  19759  efgsfo  19866  rrgsupp  20863  acsfn1p  20965  rngqiprngimf1  21503  dsmmbas2  21950  dsmmacl  21954  frlmbas  21968  frlmsslss2  21988  mplsubglem2  22215  ltbwe  22260  coe1mul2lem2  22494  scmatmats  22733  mretopd  23317  ordtbaslem  23413  ordtrest  23427  ordtrest2lem  23428  leordtval  23438  xkopt  23881  xkoco1cn  23883  xkoco2cn  23884  xkoinjcn  23913  r0cld  23964  utopsnneiplem  24473  stdbdbl  24743  minveclem3b  25656  minveclem4  25660  lhop1lem  26240  idomrootle  26398  mumul  27417  sqff1o  27418  lgsquadlem1  27616  lgsquadlem2  27617  2lgslem1a  27627  lrrecse  28207  lrrecpred  28209  plngcplem  29142  elntg2  29442  edglnl  29600  nbupgr  29804  vtxdun  29941  wwlksnextprop  30380  wpthswwlks2on  30432  rusgrnumwwlkslem  30440  rusgrnumwwlks  30445  clwlknf1oclwwlkn  30554  frcond3  30749  extwwlkfab  30832  grpoidinv2  30996  grpoinv  31006  xppreima  33118  qusker  33789  nsgqusf1olem3  33844  fedgmullem2  34140  ply1annidllem  34211  zarclsun  34380  cnvordtrestixx  34423  ordtrestNEW  34431  ordtrest2NEWlem  34432  fnrelpredd  35596  fineqvnttrclse  35650  satfv1lem  35941  satefvfmla0  35997  satefvfmla1  36004  lineunray  36727  lineelsb2  36728  linecom  36730  nmulrid  36777  ee7.2aOLD  37080  poimirlem26  38395  poimirlem27  38396  mbfposadd  38416  cnambfre  38417  itg2addnclem2  38421  iblabsnclem  38432  ftc1anclem1  38442  lfl1dim2N  39995  pmapat  40636  pmapglbx  40642  dvhb1dimN  41859  dia0  41925  mapdval2N  42503  mapdsn  42514  hlhilocv  42830  isprimroot  42959  aks6d1c6isolem3  43042  unitscyglem5  43065  istopclsd  43545  diophren  43654  rabrenfdioph  43655  pwfi2f1o  43937  idomodle  44032  hausgraph  44046  nadd1rabtr  44229  nadd1rabex  44231  nadd1suc  44233  minregex2  44375  fsovcnvlem  44853  ntrneifv3  44922  ntrneifv4  44925  clsneifv3  44950  clsneifv4  44951  neicvgfv  44961  nzss  45141  preimaiocmnf  46390  preimaicomnf  47539  smfsupxr  47644  smfliminflem  47658  sprvalpwle2  48389  fpprmod  48643  dfsclnbgr2  48762  dfvopnbgr2  48769  uspgrlimlem2  48905  rmsupp0  49298  lco0  49357  rrxlinesc  49665  rrxlinec  49666  rrx2line  49670  rrx2vlinest  49671  rrx2linest  49672  rrx2linesl  49673  rrx2linest2  49674  2sphere  49679  2sphere0  49680  line2  49682  itsclinecirc0b  49704