Theorem rabbii 3473

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3480. (Contributed by Peter Mazsa, 1-Nov-2019.)

Hypothesis

Ref	Expression
rabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rabbii	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem rabbii

Step	Hyp	Ref	Expression
1		rabbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rabbiia 3472	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-rab 3147

This theorem is referenced by:  dfdif3  4091  elneldisj  4342  elnelun  4343  dfepfr  5540  epfrc  5541  fndmdifcom  6813  fniniseg2  6832  uniordint  7521  dfoi  8975  kmlem3  9578  alephsuc3  10002  hashbclem  13811  gcdcom  15862  gcdass  15895  lcmcom  15937  lcmass  15958  acsfn0  16931  dfrhm2  19469  lbsextg  19934  dmtopon  21531  fctop2  21613  ordtrest2  21812  qtopres  22306  tsmsfbas  22736  shftmbl  24139  ppiub  25780  rpvmasum  26102  umgrislfupgrlem  26907  finsumvtxdg2ssteplem1  27327  clwwlknclwwlkdifnum  27758  clwwlknon2num  27884  dlwwlknondlwlknonf1o  28144  numclwlk1lem1  28148  aciunf1  30408  fpwrelmapffslem  30468  ordtrest2NEW  31166  unelldsys  31417  rossros  31439  aean  31503  orvcval2  31716  subfacp1lem6  32432  satfv1  32610  noextendlt  33176  nosepne  33185  nosepdm  33188  nosupbnd2lem1  33215  noetalem3  33219  itg2addnclem2  34959  scottexf  35461  scott0f  35462  rabbieq  35527  refsymrels2  35816  dfeqvrels2  35838  refrelsredund3  35884  dffunsALTV5  35935  glbconxN  36529  3anrabdioph  39399  3orrabdioph  39400  rexrabdioph  39411  2rexfrabdioph  39413  3rexfrabdioph  39414  4rexfrabdioph  39415  6rexfrabdioph  39416  7rexfrabdioph  39417  elnn0rabdioph  39420  elnnrabdioph  39424  rabren3dioph  39432  rmydioph  39631  rmxdioph  39633  expdiophlem2  39639  relintab  39963  uzmptshftfval  40698  binomcxplemdvsum  40707  binomcxp  40709  dvnprod  42254  ovnsubadd  42874  hoidmv1lelem3  42895  hoidmvlelem3  42899  ovolval3  42949  ovolval4lem2  42952  ovolval5lem3  42956  smflimlem4  43070