Theorem abbidv 2467

Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)

Hypothesis

Ref	Expression
abbidv.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
abbidv	⊢ (φ → {x ∣ ψ} = {x ∣ χ})

Distinct variable group:   φ,x

Allowed substitution hints:   ψ(x)   χ(x)

Proof of Theorem abbidv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxφ
2		abbidv.1	. 2 ⊢ (φ → (ψ ↔ χ))
3	1, 2	abbid 2466	1 ⊢ (φ → {x ∣ ψ} = {x ∣ χ})

Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642  {cab 2339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346

This theorem is referenced by:  csbeq1  3139  sbcel12g  3151  sbceqg  3152  csbeq2d  3160  csbnestgf  3184  nineq1  3234  pweq  3725  sneq  3744  csbsng  3785  rabsn  3790  csbunig  3899  unieq  3900  inteq  3929  iineq1  3983  iineq2  3986  dfiin2g  4000  iinrab  4028  cnvkeq  4215  ins2keq  4218  ins3keq  4219  imakeq1  4224  imakeq2  4225  p6eq  4238  sikeq  4241  setswith  4321  iotaeq  4347  iotabi  4348  preaddccan2lem1  4454  nnadjoin  4520  tfinnn  4534  opabbid  4624  csbxpg  4813  imaeq1  4937  imaeq2  4938  csbrng  4966  imasn  5018  fnrnfv  5364  dfimafn  5366  fnsnfv  5373  fvco2  5382  oprabbid  5563  clos1eq1  5874  clos1eq2  5875  erth  5968  qseq1  5974  qseq2  5975  mapex  6006  mapvalg  6009  ovmuc  6130  ovce  6172  addccan2nclem2  6264