Theorem rabbidva 3411

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542   ∈ wcel 2110  {crab 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-rab 3075

This theorem is referenced by:  rabbidv  3413  rabeqbidva  3420  rabbi2dva  4157  rabxfrd  5344  seinxp  5671  ordintdif  6314  f1oresrab  6996  onsucmin  7663  suppval1  7975  mptsuppd  7995  cantnflem1  9435  harsucnn  9767  dfinfre  11967  ixxin  13107  mptnn0fsuppr  13730  scshwfzeqfzo  14550  incexc2  15561  smueqlem  16208  gcdass  16266  lcmass  16330  pcneg  16586  ramval  16720  acsfn  17379  monpropd  17460  f1omvdcnv  19063  pmtrmvd  19075  submod  19185  odngen  19193  sylow3lem6  19248  efgsfo  19356  acsfn1p  20078  rrgsupp  20573  dsmmbas2  20955  dsmmacl  20959  frlmbas  20973  frlmsslss2  20993  mplsubglem2  21218  ltbwe  21256  coe1mul2lem2  21450  scmatmats  21671  mretopd  22254  ordtbaslem  22350  ordtrest  22364  ordtrest2lem  22365  leordtval  22375  xkopt  22817  xkoco1cn  22819  xkoco2cn  22820  xkoinjcn  22849  r0cld  22900  utopsnneiplem  23410  stdbdbl  23684  minveclem3b  24603  minveclem4  24607  lhop1lem  25188  mumul  26341  sqff1o  26342  lgsquadlem1  26539  lgsquadlem2  26540  2lgslem1a  26550  elntg2  27364  edglnl  27524  nbupgr  27722  vtxdun  27859  wwlksnextprop  28286  wpthswwlks2on  28335  rusgrnumwwlkslem  28343  rusgrnumwwlks  28348  clwlknf1oclwwlkn  28457  frcond3  28642  extwwlkfab  28725  grpoidinv2  28886  grpoinv  28896  xppreima  30992  qusker  31558  nsgqusf1olem3  31609  fedgmullem2  31720  zarclsun  31829  cnvordtrestixx  31872  ordtrestNEW  31880  ordtrest2NEWlem  31881  fnrelpredd  33070  satfv1lem  33333  satefvfmla0  33389  satefvfmla1  33396  lrrecse  34108  lrrecpred  34110  lineunray  34458  lineelsb2  34459  linecom  34461  ee7.2aOLD  34659  poimirlem26  35812  poimirlem27  35813  mbfposadd  35833  cnambfre  35834  itg2addnclem2  35838  iblabsnclem  35849  ftc1anclem1  35859  lfl1dim2N  37145  pmapat  37786  pmapglbx  37792  dvhb1dimN  39009  dia0  39075  mapdval2N  39653  mapdsn  39664  hlhilocv  39984  istopclsd  40531  diophren  40644  rabrenfdioph  40645  pwfi2f1o  40930  idomrootle  41029  idomodle  41030  hausgraph  41046  fsovcnvlem  41603  ntrneifv3  41674  ntrneifv4  41677  clsneifv3  41702  clsneifv4  41703  neicvgfv  41713  nzss  41917  preimaiocmnf  43081  preimaicomnf  44228  smfsupxr  44328  smfliminflem  44342  sprvalpwle2  44920  fpprmod  45158  rmsupp0  45683  lco0  45747  rrxlinesc  46060  rrxlinec  46061  rrx2line  46065  rrx2vlinest  46066  rrx2linest  46067  rrx2linesl  46068  rrx2linest2  46069  2sphere  46074  2sphere0  46075  line2  46077  itsclinecirc0b  46099