Theorem rabbidva 3409

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

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

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 3403

This theorem is referenced by:  rabbidv  3410  rabeqbidva  3419  rabeqbidvaOLD  3420  rabbi2dva  4185  rabxfrd  5367  seinxp  5715  ordintdif  6371  f1oresrab  7081  onsucmin  7776  suppval1  8122  mptsuppd  8143  naddasslem1  8635  naddasslem2  8636  naddsuc2  8642  cantnflem1  9618  harsucnn  9927  dfinfre  12140  ixxin  13299  mptnn0fsuppr  13940  scshwfzeqfzo  14768  incexc2  15780  smueqlem  16436  gcdass  16493  lcmass  16560  pcneg  16821  ramval  16955  acsfn  17600  monpropd  17679  f1omvdcnv  19358  pmtrmvd  19370  submod  19483  odngen  19491  sylow3lem6  19546  efgsfo  19653  rrgsupp  20621  acsfn1p  20719  rngqiprngimf1  21242  dsmmbas2  21679  dsmmacl  21683  frlmbas  21697  frlmsslss2  21717  mplsubglem2  21943  ltbwe  21984  coe1mul2lem2  22187  scmatmats  22431  mretopd  23012  ordtbaslem  23108  ordtrest  23122  ordtrest2lem  23123  leordtval  23133  xkopt  23575  xkoco1cn  23577  xkoco2cn  23578  xkoinjcn  23607  r0cld  23658  utopsnneiplem  24168  stdbdbl  24438  minveclem3b  25361  minveclem4  25365  lhop1lem  25951  idomrootle  26111  mumul  27124  sqff1o  27125  lgsquadlem1  27324  lgsquadlem2  27325  2lgslem1a  27335  lrrecse  27889  lrrecpred  27891  elntg2  28965  edglnl  29123  nbupgr  29324  vtxdun  29462  wwlksnextprop  29892  wpthswwlks2on  29941  rusgrnumwwlkslem  29949  rusgrnumwwlks  29954  clwlknf1oclwwlkn  30063  frcond3  30248  extwwlkfab  30331  grpoidinv2  30494  grpoinv  30504  xppreima  32619  qusker  33313  nsgqusf1olem3  33379  fedgmullem2  33619  ply1annidllem  33684  zarclsun  33853  cnvordtrestixx  33896  ordtrestNEW  33904  ordtrest2NEWlem  33905  fnrelpredd  35072  satfv1lem  35342  satefvfmla0  35398  satefvfmla1  35405  lineunray  36128  lineelsb2  36129  linecom  36131  ee7.2aOLD  36442  poimirlem26  37633  poimirlem27  37634  mbfposadd  37654  cnambfre  37655  itg2addnclem2  37659  iblabsnclem  37670  ftc1anclem1  37680  lfl1dim2N  39108  pmapat  39750  pmapglbx  39756  dvhb1dimN  40973  dia0  41039  mapdval2N  41617  mapdsn  41628  hlhilocv  41944  isprimroot  42074  aks6d1c6isolem3  42157  unitscyglem5  42180  istopclsd  42681  diophren  42794  rabrenfdioph  42795  pwfi2f1o  43078  idomodle  43173  hausgraph  43187  nadd1rabtr  43370  nadd1rabex  43372  nadd1suc  43374  minregex2  43517  fsovcnvlem  43995  ntrneifv3  44064  ntrneifv4  44067  clsneifv3  44092  clsneifv4  44093  neicvgfv  44103  nzss  44299  preimaiocmnf  45551  preimaicomnf  46702  smfsupxr  46807  smfliminflem  46821  sprvalpwle2  47483  fpprmod  47721  dfsclnbgr2  47839  dfvopnbgr2  47846  uspgrlimlem2  47981  rmsupp0  48349  lco0  48409  rrxlinesc  48717  rrxlinec  48718  rrx2line  48722  rrx2vlinest  48723  rrx2linest  48724  rrx2linesl  48725  rrx2linest2  48726  2sphere  48731  2sphere0  48732  line2  48734  itsclinecirc0b  48756