Theorem rabbii 3427

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3429. (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 3426	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {crab 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rab 3423

This theorem is referenced by:  rabbieq  3430  dfdif3OLD  4079  dfepfr  5646  epfrc  5647  fndmdifcom  7039  fniniseg2  7058  uniordint  7800  naddov3  8667  dfoi  9473  kmlem3  10136  alephsuc3  10565  hashbclem  14489  gcdcom  16571  gcdass  16605  lcmcom  16651  lcmass  16672  acsfn0  17716  dfinito2  18060  dftermo2  18061  dfrhm2  20556  lbsextg  21264  dmtopon  23049  fctop2  23131  ordtrest2  23330  qtopres  23824  tsmsfbas  24254  shftmbl  25666  ppiub  27334  rpvmasum  27656  noextendlt  27799  nosepne  27810  nosepdm  27814  nosupbnd2lem1  27845  noinfbnd2lem1  27860  noetasuplem4  27866  umgrislfupgrlem  29413  finsumvtxdg2ssteplem1  29836  clwwlknclwwlkdifnum  30272  clwwlknon2num  30397  dlwwlknondlwlknonf1o  30657  numclwlk1lem1  30661  3unrab  32790  aciunf1  32949  fpwrelmapffslem  33018  constrcbvlem  34090  ordtrest2NEW  34258  unelldsys  34493  rossros  34515  aean  34579  orvcval2  34794  subfacp1lem6  35610  satfv1  35788  itg2addnclem2  38246  scottexf  38742  scott0f  38743  refsymrels2  39223  dfeqvrels2  39246  refrelsredund3  39292  dffunsALTV5  39346  glbconxN  40077  primrootsunit1  42789  primrootsunit  42790  3anrabdioph  43440  3orrabdioph  43441  rexrabdioph  43448  2rexfrabdioph  43450  3rexfrabdioph  43451  4rexfrabdioph  43452  6rexfrabdioph  43453  7rexfrabdioph  43454  elnn0rabdioph  43457  elnnrabdioph  43461  rabren3dioph  43469  rmydioph  43668  rmxdioph  43670  expdiophlem2  43676  onuniintrab  43880  relintab  44236  sqrtcvallem1  44284  uzmptshftfval  44983  binomcxplemdvsum  44992  binomcxp  44994  dvnprod  46590  fourierdlem113  46860  ovnsubadd  47213  hoidmv1lelem3  47234  hoidmvlelem3  47238  ovolval3  47288  ovolval4lem2  47291  ovolval5lem3  47295  smflimlem4  47415