Theorem rabbidva 3440

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 580	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rabbidva2 3435	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434

This theorem is referenced by:  rabbidv  3441  rabeqbidva  3449  rabbi2dva  4218  rabxfrd  5416  seinxp  5760  ordintdif  6415  f1oresrab  7125  onsucmin  7809  suppval1  8152  mptsuppd  8172  naddasslem1  8693  naddasslem2  8694  cantnflem1  9684  harsucnn  9993  dfinfre  12195  ixxin  13341  mptnn0fsuppr  13964  scshwfzeqfzo  14777  incexc2  15784  smueqlem  16431  gcdass  16489  lcmass  16551  pcneg  16807  ramval  16941  acsfn  17603  monpropd  17684  f1omvdcnv  19312  pmtrmvd  19324  submod  19437  odngen  19445  sylow3lem6  19500  efgsfo  19607  acsfn1p  20415  rrgsupp  20907  dsmmbas2  21292  dsmmacl  21296  frlmbas  21310  frlmsslss2  21330  mplsubglem2  21560  ltbwe  21599  coe1mul2lem2  21790  scmatmats  22013  mretopd  22596  ordtbaslem  22692  ordtrest  22706  ordtrest2lem  22707  leordtval  22717  xkopt  23159  xkoco1cn  23161  xkoco2cn  23162  xkoinjcn  23191  r0cld  23242  utopsnneiplem  23752  stdbdbl  24026  minveclem3b  24945  minveclem4  24949  lhop1lem  25530  mumul  26685  sqff1o  26686  lgsquadlem1  26883  lgsquadlem2  26884  2lgslem1a  26894  lrrecse  27426  lrrecpred  27428  elntg2  28243  edglnl  28403  nbupgr  28601  vtxdun  28738  wwlksnextprop  29166  wpthswwlks2on  29215  rusgrnumwwlkslem  29223  rusgrnumwwlks  29228  clwlknf1oclwwlkn  29337  frcond3  29522  extwwlkfab  29605  grpoidinv2  29768  grpoinv  29778  xppreima  31871  qusker  32464  nsgqusf1olem3  32526  fedgmullem2  32715  ply1annidllem  32762  zarclsun  32850  cnvordtrestixx  32893  ordtrestNEW  32901  ordtrest2NEWlem  32902  fnrelpredd  34092  satfv1lem  34353  satefvfmla0  34409  satefvfmla1  34416  lineunray  35119  lineelsb2  35120  linecom  35122  ee7.2aOLD  35346  poimirlem26  36514  poimirlem27  36515  mbfposadd  36535  cnambfre  36536  itg2addnclem2  36540  iblabsnclem  36551  ftc1anclem1  36561  lfl1dim2N  37992  pmapat  38634  pmapglbx  38640  dvhb1dimN  39857  dia0  39923  mapdval2N  40501  mapdsn  40512  hlhilocv  40832  istopclsd  41438  diophren  41551  rabrenfdioph  41552  pwfi2f1o  41838  idomrootle  41937  idomodle  41938  hausgraph  41954  nadd1rabtr  42138  nadd1rabex  42140  nadd1suc  42142  naddsuc2  42143  minregex2  42286  fsovcnvlem  42764  ntrneifv3  42833  ntrneifv4  42836  clsneifv3  42861  clsneifv4  42862  neicvgfv  42872  nzss  43076  preimaiocmnf  44274  preimaicomnf  45427  smfsupxr  45532  smfliminflem  45546  sprvalpwle2  46157  fpprmod  46395  rngqiprngimf1  46785  rmsupp0  47044  lco0  47108  rrxlinesc  47421  rrxlinec  47422  rrx2line  47426  rrx2vlinest  47427  rrx2linest  47428  rrx2linesl  47429  rrx2linest2  47430  2sphere  47435  2sphere0  47436  line2  47438  itsclinecirc0b  47460