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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {crab 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-rab 3396

This theorem is referenced by:  rabbidv  3402  rabeqbidva  3411  rabeqbidvaOLD  3412  rabbi2dva  4173  rabxfrd  5353  seinxp  5698  ordintdif  6357  f1oresrab  7060  onsucmin  7751  suppval1  8096  mptsuppd  8117  naddasslem1  8609  naddasslem2  8610  naddsuc2  8616  cantnflem1  9579  harsucnn  9891  dfinfre  12103  ixxin  13262  mptnn0fsuppr  13906  scshwfzeqfzo  14733  incexc2  15745  smueqlem  16401  gcdass  16458  lcmass  16525  pcneg  16786  ramval  16920  acsfn  17565  monpropd  17644  f1omvdcnv  19356  pmtrmvd  19368  submod  19481  odngen  19489  sylow3lem6  19544  efgsfo  19651  rrgsupp  20616  acsfn1p  20714  rngqiprngimf1  21237  dsmmbas2  21674  dsmmacl  21678  frlmbas  21692  frlmsslss2  21712  mplsubglem2  21938  ltbwe  21979  coe1mul2lem2  22182  scmatmats  22426  mretopd  23007  ordtbaslem  23103  ordtrest  23117  ordtrest2lem  23118  leordtval  23128  xkopt  23570  xkoco1cn  23572  xkoco2cn  23573  xkoinjcn  23602  r0cld  23653  utopsnneiplem  24162  stdbdbl  24432  minveclem3b  25355  minveclem4  25359  lhop1lem  25945  idomrootle  26105  mumul  27118  sqff1o  27119  lgsquadlem1  27318  lgsquadlem2  27319  2lgslem1a  27329  lrrecse  27885  lrrecpred  27887  elntg2  28963  edglnl  29121  nbupgr  29322  vtxdun  29460  wwlksnextprop  29890  wpthswwlks2on  29942  rusgrnumwwlkslem  29950  rusgrnumwwlks  29955  clwlknf1oclwwlkn  30064  frcond3  30249  extwwlkfab  30332  grpoidinv2  30495  grpoinv  30505  xppreima  32627  qusker  33314  nsgqusf1olem3  33380  fedgmullem2  33643  ply1annidllem  33714  zarclsun  33883  cnvordtrestixx  33926  ordtrestNEW  33934  ordtrest2NEWlem  33935  fnrelpredd  35102  fineqvnttrclse  35144  satfv1lem  35406  satefvfmla0  35462  satefvfmla1  35469  lineunray  36191  lineelsb2  36192  linecom  36194  ee7.2aOLD  36505  poimirlem26  37696  poimirlem27  37697  mbfposadd  37717  cnambfre  37718  itg2addnclem2  37722  iblabsnclem  37733  ftc1anclem1  37743  lfl1dim2N  39231  pmapat  39872  pmapglbx  39878  dvhb1dimN  41095  dia0  41161  mapdval2N  41739  mapdsn  41750  hlhilocv  42066  isprimroot  42196  aks6d1c6isolem3  42279  unitscyglem5  42302  istopclsd  42803  diophren  42916  rabrenfdioph  42917  pwfi2f1o  43199  idomodle  43294  hausgraph  43308  nadd1rabtr  43491  nadd1rabex  43493  nadd1suc  43495  minregex2  43638  fsovcnvlem  44116  ntrneifv3  44185  ntrneifv4  44188  clsneifv3  44213  clsneifv4  44214  neicvgfv  44224  nzss  44420  preimaiocmnf  45670  preimaicomnf  46819  smfsupxr  46924  smfliminflem  46938  sprvalpwle2  47599  fpprmod  47837  dfsclnbgr2  47956  dfvopnbgr2  47963  uspgrlimlem2  48099  rmsupp0  48478  lco0  48538  rrxlinesc  48846  rrxlinec  48847  rrx2line  48851  rrx2vlinest  48852  rrx2linest  48853  rrx2linesl  48854  rrx2linest2  48855  2sphere  48860  2sphere0  48861  line2  48863  itsclinecirc0b  48885