Theorem rabbidva 3396

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3391

This theorem is referenced by:  rabbidv  3397  rabeqbidva  3406  rabeqbidvaOLD  3407  rabbi2dva  4167  rabxfrd  5355  seinxp  5709  ordintdif  6369  f1oresrab  7075  onsucmin  7766  suppval1  8110  mptsuppd  8131  naddasslem1  8624  naddasslem2  8625  naddsuc2  8631  cantnflem1  9604  harsucnn  9916  dfinfre  12131  ixxin  13309  mptnn0fsuppr  13955  scshwfzeqfzo  14782  incexc2  15797  smueqlem  16453  gcdass  16510  lcmass  16577  pcneg  16839  ramval  16973  acsfn  17619  monpropd  17698  f1omvdcnv  19413  pmtrmvd  19425  submod  19538  odngen  19546  sylow3lem6  19601  efgsfo  19708  rrgsupp  20672  acsfn1p  20770  rngqiprngimf1  21293  dsmmbas2  21730  dsmmacl  21734  frlmbas  21748  frlmsslss2  21768  mplsubglem2  21992  ltbwe  22035  coe1mul2lem2  22246  scmatmats  22489  mretopd  23070  ordtbaslem  23166  ordtrest  23180  ordtrest2lem  23181  leordtval  23191  xkopt  23633  xkoco1cn  23635  xkoco2cn  23636  xkoinjcn  23665  r0cld  23716  utopsnneiplem  24225  stdbdbl  24495  minveclem3b  25408  minveclem4  25412  lhop1lem  25993  idomrootle  26151  mumul  27161  sqff1o  27162  lgsquadlem1  27360  lgsquadlem2  27361  2lgslem1a  27371  lrrecse  27951  lrrecpred  27953  elntg2  29071  edglnl  29229  nbupgr  29430  vtxdun  29568  wwlksnextprop  29998  wpthswwlks2on  30050  rusgrnumwwlkslem  30058  rusgrnumwwlks  30063  clwlknf1oclwwlkn  30172  frcond3  30357  extwwlkfab  30440  grpoidinv2  30604  grpoinv  30614  xppreima  32736  qusker  33427  nsgqusf1olem3  33493  fedgmullem2  33793  ply1annidllem  33864  zarclsun  34033  cnvordtrestixx  34076  ordtrestNEW  34084  ordtrest2NEWlem  34085  fnrelpredd  35253  fineqvnttrclse  35287  satfv1lem  35563  satefvfmla0  35619  satefvfmla1  35626  lineunray  36348  lineelsb2  36349  linecom  36351  ee7.2aOLD  36662  poimirlem26  37984  poimirlem27  37985  mbfposadd  38005  cnambfre  38006  itg2addnclem2  38010  iblabsnclem  38021  ftc1anclem1  38031  lfl1dim2N  39585  pmapat  40226  pmapglbx  40232  dvhb1dimN  41449  dia0  41515  mapdval2N  42093  mapdsn  42104  hlhilocv  42420  isprimroot  42549  aks6d1c6isolem3  42632  unitscyglem5  42655  istopclsd  43149  diophren  43262  rabrenfdioph  43263  pwfi2f1o  43545  idomodle  43640  hausgraph  43654  nadd1rabtr  43837  nadd1rabex  43839  nadd1suc  43841  minregex2  43983  fsovcnvlem  44461  ntrneifv3  44530  ntrneifv4  44533  clsneifv3  44558  clsneifv4  44559  neicvgfv  44569  nzss  44765  preimaiocmnf  46011  preimaicomnf  47160  smfsupxr  47265  smfliminflem  47279  sprvalpwle2  47964  fpprmod  48218  dfsclnbgr2  48337  dfvopnbgr2  48344  uspgrlimlem2  48480  rmsupp0  48859  lco0  48918  rrxlinesc  49226  rrxlinec  49227  rrx2line  49231  rrx2vlinest  49232  rrx2linest  49233  rrx2linesl  49234  rrx2linest2  49235  2sphere  49240  2sphere0  49241  line2  49243  itsclinecirc0b  49265