Theorem rabbidva 3378

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2112  {crab 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-rab 3060

This theorem is referenced by:  rabbidv  3380  rabeqbidva  3387  rabbi2dva  4118  rabxfrd  5295  seinxp  5617  ordintdif  6240  f1oresrab  6920  onsucmin  7578  suppval1  7887  mptsuppd  7907  cantnflem1  9282  harsucnn  9579  dfinfre  11778  ixxin  12917  mptnn0fsuppr  13537  scshwfzeqfzo  14356  incexc2  15365  smueqlem  16012  gcdass  16070  lcmass  16134  pcneg  16390  ramval  16524  acsfn  17116  monpropd  17196  f1omvdcnv  18790  pmtrmvd  18802  submod  18912  odngen  18920  sylow3lem6  18975  efgsfo  19083  acsfn1p  19797  rrgsupp  20283  dsmmbas2  20653  dsmmacl  20657  frlmbas  20671  frlmsslss2  20691  mplsubglem2  20917  ltbwe  20955  coe1mul2lem2  21143  scmatmats  21362  mretopd  21943  ordtbaslem  22039  ordtrest  22053  ordtrest2lem  22054  leordtval  22064  xkopt  22506  xkoco1cn  22508  xkoco2cn  22509  xkoinjcn  22538  r0cld  22589  utopsnneiplem  23099  stdbdbl  23369  minveclem3b  24279  minveclem4  24283  lhop1lem  24864  mumul  26017  sqff1o  26018  lgsquadlem1  26215  lgsquadlem2  26216  2lgslem1a  26226  elntg2  27030  edglnl  27188  nbupgr  27386  vtxdun  27523  wwlksnextprop  27950  wpthswwlks2on  27999  rusgrnumwwlkslem  28007  rusgrnumwwlks  28012  clwlknf1oclwwlkn  28121  frcond3  28306  extwwlkfab  28389  grpoidinv2  28550  grpoinv  28560  xppreima  30656  qusker  31217  nsgqusf1olem3  31268  fedgmullem2  31379  zarclsun  31488  cnvordtrestixx  31531  ordtrestNEW  31539  ordtrest2NEWlem  31540  fnrelpredd  32728  satfv1lem  32991  satefvfmla0  33047  satefvfmla1  33054  lrrecse  33785  lrrecpred  33787  lineunray  34135  lineelsb2  34136  linecom  34138  ee7.2aOLD  34336  poimirlem26  35489  poimirlem27  35490  mbfposadd  35510  cnambfre  35511  itg2addnclem2  35515  iblabsnclem  35526  ftc1anclem1  35536  lfl1dim2N  36822  pmapat  37463  pmapglbx  37469  dvhb1dimN  38686  dia0  38752  mapdval2N  39330  mapdsn  39341  hlhilocv  39657  istopclsd  40166  diophren  40279  rabrenfdioph  40280  pwfi2f1o  40565  idomrootle  40664  idomodle  40665  hausgraph  40681  fsovcnvlem  41239  ntrneifv3  41310  ntrneifv4  41313  clsneifv3  41338  clsneifv4  41339  neicvgfv  41349  nzss  41549  preimaiocmnf  42715  preimaicomnf  43864  smfsupxr  43964  smfliminflem  43978  sprvalpwle2  44557  fpprmod  44795  rmsupp0  45320  lco0  45384  rrxlinesc  45697  rrxlinec  45698  rrx2line  45702  rrx2vlinest  45703  rrx2linest  45704  rrx2linesl  45705  rrx2linest2  45706  2sphere  45711  2sphere0  45712  line2  45714  itsclinecirc0b  45736