Theorem rabbidva 3422

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is used by:  rabbidv  3423  rabeqbidva  3432  rabbi2dva  4125  rabxfrd  5386  seinxp  5743  ordintdif  6440  f1oresrab  7160  onsucmin  7866  suppval1  8221  mptsuppd  8242  naddasslem1  8742  naddasslem2  8743  naddsuc2  8749  cantnflem1  9727  harsucnn  10118  dfinfre  12338  ixxin  13533  mptnn0fsuppr  14182  scshwfzeqfzo  15019  incexc2  16051  smueqlem  16704  gcdass  16764  lcmass  16833  pcneg  17096  ramval  17230  acsfn  17883  monpropd  17962  f1omvdcnv  19709  pmtrmvd  19721  submod  19834  odngen  19842  sylow3lem6  19897  efgsfo  20004  rrgsupp  21004  acsfn1p  21107  rngqiprngimf1  21647  dsmmbas2  22098  dsmmacl  22102  frlmbas  22116  frlmsslss2  22136  mplsubglem2  22363  ltbwe  22408  coe1mul2lem2  22642  scmatmats  22881  mretopd  23465  ordtbaslem  23561  ordtrest  23575  ordtrest2lem  23576  leordtval  23586  xkopt  24029  xkoco1cn  24031  xkoco2cn  24032  xkoinjcn  24061  r0cld  24112  utopsnneiplem  24621  stdbdbl  24891  minveclem3b  25804  minveclem4  25808  lhop1lem  26388  idomrootle  26546  mumul  27565  sqff1o  27566  lgsquadlem1  27764  lgsquadlem2  27765  2lgslem1a  27775  lrrecse  28385  lrrecpred  28387  plngcplem  29320  elntg2  29620  edglnl  29778  nbupgr  29982  vtxdun  30119  wwlksnextprop  30558  wpthswwlks2on  30610  rusgrnumwwlkslem  30618  rusgrnumwwlks  30623  clwlknf1oclwwlkn  30732  frcond3  30927  extwwlkfab  31010  grpoidinv2  31174  grpoinv  31184  xppreima  33337  qusker  34014  nsgqusf1olem3  34070  fedgmullem2  34373  ply1annidllem  34444  zarclsun  34613  cnvordtrestixx  34656  ordtrestNEW  34664  ordtrest2NEWlem  34665  fnrelpredd  35845  fineqvnttrclse  35933  satfv1lem  36335  satefvfmla0  36391  satefvfmla1  36398  lineunray  37127  lineelsb2  37128  linecom  37130  nmulrid  37161  ee7.2aOLD  37464  poimirlem26  38832  poimirlem27  38833  mbfposadd  38853  cnambfre  38854  itg2addnclem2  38858  iblabsnclem  38869  ftc1anclem1  38879  lfl1dim2N  40445  pmapat  41086  pmapglbx  41092  dvhb1dimN  42309  dia0  42375  mapdval2N  42953  mapdsn  42964  hlhilocv  43280  isprimroot  43409  aks6d1c6isolem3  43492  unitscyglem5  43515  frlmnzcoordsca  43924  istopclsd  43977  diophren  44086  rabrenfdioph  44087  pwfi2f1o  44364  idomodle  44454  hausgraph  44468  nadd1rabtr  44651  nadd1rabex  44653  nadd1suc  44655  minregex2  44797  fsovcnvlem  45274  ntrneifv3  45343  ntrneifv4  45346  clsneifv3  45371  clsneifv4  45372  neicvgfv  45382  nzss  45562  preimaiocmnf  46845  preimaicomnf  47994  smfsupxr  48099  smfliminflem  48113  sprvalpwle2  48844  fpprmod  49098  dfsclnbgr2  49217  dfvopnbgr2  49224  uspgrlimlem2  49360  rmsupp0  49811  lco0  49870  rrxlinesc  50179  rrxlinec  50180  rrx2line  50183  rrx2vlinest  50184  rrx2linest  50185  rrx2linesl  50186  rrx2linest2  50187  2sphere  50192  2sphere0  50193  line2  50195  itsclinecirc0b  50217