Theorem rabbidva 3163

Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 28-Nov-2003.)

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	ralrimiva 2949	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒))
3		rabbi 3097	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
4	2, 3	sylib 207	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-rab 2905

This theorem is referenced by:  rabbidv  3164  rabeqbidva  3169  rabbi2dva  3783  rabxfrd  4815  seinxp  5108  ordintdif  5691  f1oresrab  6302  onsucmin  6913  suppval1  7188  mptsuppd  7205  cantnflem1  8469  dfinfre  10881  ixxin  12063  mptnn0fsuppr  12661  scshwfzeqfzo  13423  incexc2  14409  smueqlem  15050  gcdass  15102  lcmass  15165  pcneg  15416  ramval  15550  acsfn  16143  monpropd  16220  f1omvdcnv  17687  pmtrmvd  17699  submod  17807  odngen  17815  sylow3lem6  17870  efgsfo  17975  rrgsupp  19112  mplsubglem2  19257  ltbwe  19293  coe1mul2lem2  19459  dsmmbas2  19900  dsmmacl  19904  frlmbas  19918  frlmsslss2  19933  scmatmats  20136  mretopd  20706  ordtbaslem  20802  ordtrest  20816  ordtrest2lem  20817  leordtval  20827  xkopt  21268  xkoco1cn  21270  xkoco2cn  21271  xkoinjcn  21300  r0cld  21351  utopsnneiplem  21861  stdbdbl  22132  minveclem3b  23007  minveclem4  23011  lhop1lem  23580  mumul  24707  sqff1o  24708  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1a  24916  wwlkextprop  26272  vdgrun  26428  vdgrfiun  26429  rusgranumwlklem0  26475  rusgranumwlks  26483  frisusgranb  26524  extwwlkfab  26617  grpoidinv2  26753  grpoinv  26763  xppreima  28829  cnvordtrestixx  29287  ordtrestNEW  29295  ordtrest2NEWlem  29296  lineunray  31424  lineelsb2  31425  linecom  31427  ee7.2aOLD  31630  poimirlem26  32605  poimirlem27  32606  mbfposadd  32627  cnambfre  32628  itg2addnclem2  32632  iblabsnclem  32643  ftc1anclem1  32655  lfl1dim2N  33427  pmapat  34067  pmapglbx  34073  dvhb1dimN  35292  dia0  35359  mapdval2N  35937  mapdsn  35948  hlhilocv  36267  istopclsd  36281  diophren  36395  rabrenfdioph  36396  pwfi2f1o  36684  acsfn1p  36788  idomrootle  36792  idomodle  36793  hausgraph  36809  fsovcnvlem  37327  ntrneifv3  37400  ntrneifv4  37403  clsneifv3  37428  clsneifv4  37429  neicvgfv  37439  nzss  37538  preimaicomnf  39599  nbupgr  40566  isuvtxa  40621  vtxdun  40696  wwlksnextprop  41118  wpthswwlks2on  41164  rusgrnumwwlks  41177  frcond3  41440  av-extwwlkfab  41520  rmsupp0  41943  lco0  42010