Theorem rabbidva 3443

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-rab 3437

This theorem is referenced by:  rabbidv  3444  rabeqbidva  3453  rabeqbidvaOLD  3454  rabbi2dva  4226  rabxfrd  5417  seinxp  5769  ordintdif  6434  f1oresrab  7147  onsucmin  7841  suppval1  8191  mptsuppd  8212  naddasslem1  8732  naddasslem2  8733  naddsuc2  8739  cantnflem1  9729  harsucnn  10038  dfinfre  12249  ixxin  13404  mptnn0fsuppr  14040  scshwfzeqfzo  14865  incexc2  15874  smueqlem  16527  gcdass  16584  lcmass  16651  pcneg  16912  ramval  17046  acsfn  17702  monpropd  17781  f1omvdcnv  19462  pmtrmvd  19474  submod  19587  odngen  19595  sylow3lem6  19650  efgsfo  19757  rrgsupp  20701  acsfn1p  20800  rngqiprngimf1  21310  dsmmbas2  21757  dsmmacl  21761  frlmbas  21775  frlmsslss2  21795  mplsubglem2  22021  ltbwe  22062  coe1mul2lem2  22271  scmatmats  22517  mretopd  23100  ordtbaslem  23196  ordtrest  23210  ordtrest2lem  23211  leordtval  23221  xkopt  23663  xkoco1cn  23665  xkoco2cn  23666  xkoinjcn  23695  r0cld  23746  utopsnneiplem  24256  stdbdbl  24530  minveclem3b  25462  minveclem4  25466  lhop1lem  26052  idomrootle  26212  mumul  27224  sqff1o  27225  lgsquadlem1  27424  lgsquadlem2  27425  2lgslem1a  27435  lrrecse  27975  lrrecpred  27977  elntg2  29000  edglnl  29160  nbupgr  29361  vtxdun  29499  wwlksnextprop  29932  wpthswwlks2on  29981  rusgrnumwwlkslem  29989  rusgrnumwwlks  29994  clwlknf1oclwwlkn  30103  frcond3  30288  extwwlkfab  30371  grpoidinv2  30534  grpoinv  30544  xppreima  32655  qusker  33377  nsgqusf1olem3  33443  fedgmullem2  33681  ply1annidllem  33744  zarclsun  33869  cnvordtrestixx  33912  ordtrestNEW  33920  ordtrest2NEWlem  33921  fnrelpredd  35103  satfv1lem  35367  satefvfmla0  35423  satefvfmla1  35430  lineunray  36148  lineelsb2  36149  linecom  36151  ee7.2aOLD  36462  poimirlem26  37653  poimirlem27  37654  mbfposadd  37674  cnambfre  37675  itg2addnclem2  37679  iblabsnclem  37690  ftc1anclem1  37700  lfl1dim2N  39123  pmapat  39765  pmapglbx  39771  dvhb1dimN  40988  dia0  41054  mapdval2N  41632  mapdsn  41643  hlhilocv  41963  isprimroot  42094  aks6d1c6isolem3  42177  unitscyglem5  42200  istopclsd  42711  diophren  42824  rabrenfdioph  42825  pwfi2f1o  43108  idomodle  43203  hausgraph  43217  nadd1rabtr  43401  nadd1rabex  43403  nadd1suc  43405  minregex2  43548  fsovcnvlem  44026  ntrneifv3  44095  ntrneifv4  44098  clsneifv3  44123  clsneifv4  44124  neicvgfv  44134  nzss  44336  preimaiocmnf  45574  preimaicomnf  46726  smfsupxr  46831  smfliminflem  46845  sprvalpwle2  47476  fpprmod  47714  dfsclnbgr2  47832  dfvopnbgr2  47839  uspgrlimlem2  47956  rmsupp0  48284  lco0  48344  rrxlinesc  48656  rrxlinec  48657  rrx2line  48661  rrx2vlinest  48662  rrx2linest  48663  rrx2linesl  48664  rrx2linest2  48665  2sphere  48670  2sphere0  48671  line2  48673  itsclinecirc0b  48695