Theorem rabbidva 3412

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

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

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 3406

This theorem is referenced by:  rabbidv  3413  rabeqbidva  3422  rabeqbidvaOLD  3423  rabbi2dva  4189  rabxfrd  5372  seinxp  5722  ordintdif  6383  f1oresrab  7099  onsucmin  7796  suppval1  8145  mptsuppd  8166  naddasslem1  8658  naddasslem2  8659  naddsuc2  8665  cantnflem1  9642  harsucnn  9951  dfinfre  12164  ixxin  13323  mptnn0fsuppr  13964  scshwfzeqfzo  14792  incexc2  15804  smueqlem  16460  gcdass  16517  lcmass  16584  pcneg  16845  ramval  16979  acsfn  17620  monpropd  17699  f1omvdcnv  19374  pmtrmvd  19386  submod  19499  odngen  19507  sylow3lem6  19562  efgsfo  19669  rrgsupp  20610  acsfn1p  20708  rngqiprngimf1  21210  dsmmbas2  21646  dsmmacl  21650  frlmbas  21664  frlmsslss2  21684  mplsubglem2  21910  ltbwe  21951  coe1mul2lem2  22154  scmatmats  22398  mretopd  22979  ordtbaslem  23075  ordtrest  23089  ordtrest2lem  23090  leordtval  23100  xkopt  23542  xkoco1cn  23544  xkoco2cn  23545  xkoinjcn  23574  r0cld  23625  utopsnneiplem  24135  stdbdbl  24405  minveclem3b  25328  minveclem4  25332  lhop1lem  25918  idomrootle  26078  mumul  27091  sqff1o  27092  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1a  27302  lrrecse  27849  lrrecpred  27851  elntg2  28912  edglnl  29070  nbupgr  29271  vtxdun  29409  wwlksnextprop  29842  wpthswwlks2on  29891  rusgrnumwwlkslem  29899  rusgrnumwwlks  29904  clwlknf1oclwwlkn  30013  frcond3  30198  extwwlkfab  30281  grpoidinv2  30444  grpoinv  30454  xppreima  32569  qusker  33320  nsgqusf1olem3  33386  fedgmullem2  33626  ply1annidllem  33691  zarclsun  33860  cnvordtrestixx  33903  ordtrestNEW  33911  ordtrest2NEWlem  33912  fnrelpredd  35079  satfv1lem  35349  satefvfmla0  35405  satefvfmla1  35412  lineunray  36135  lineelsb2  36136  linecom  36138  ee7.2aOLD  36449  poimirlem26  37640  poimirlem27  37641  mbfposadd  37661  cnambfre  37662  itg2addnclem2  37666  iblabsnclem  37677  ftc1anclem1  37687  lfl1dim2N  39115  pmapat  39757  pmapglbx  39763  dvhb1dimN  40980  dia0  41046  mapdval2N  41624  mapdsn  41635  hlhilocv  41951  isprimroot  42081  aks6d1c6isolem3  42164  unitscyglem5  42187  istopclsd  42688  diophren  42801  rabrenfdioph  42802  pwfi2f1o  43085  idomodle  43180  hausgraph  43194  nadd1rabtr  43377  nadd1rabex  43379  nadd1suc  43381  minregex2  43524  fsovcnvlem  44002  ntrneifv3  44071  ntrneifv4  44074  clsneifv3  44099  clsneifv4  44100  neicvgfv  44110  nzss  44306  preimaiocmnf  45558  preimaicomnf  46709  smfsupxr  46814  smfliminflem  46828  sprvalpwle2  47490  fpprmod  47728  dfsclnbgr2  47846  dfvopnbgr2  47853  uspgrlimlem2  47988  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