Theorem opabbidv 4155

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.)

Hypothesis

Ref	Expression
opabbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
opabbidv	|- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)   ch( x, y)

Proof of Theorem opabbidv

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 |- F/ x ph
2		nfv 1576	. 2 |- F/ y ph
3		opabbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
4	1, 2, 3	opabbid 4154	1 |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   {copab 4149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-opab 4151

This theorem is referenced by:  opabbii  4156  csbopabg  4167  xpeq1  4739  xpeq2  4740  opabbi2dv  4879  csbcnvg  4914  resopab2  5060  mptcnv  5139  cores  5240  xpcom  5283  dffn5im  5691  f1oiso2  5967  f1ocnvd  6224  ofreq  6238  f1od2  6399  shftfvalg  11378  shftfval  11381  2shfti  11391  prdsex  13351  prdsval  13355  releqgg  13806  eqgex  13807  eqgfval  13808  dvdsrvald  14106  dvdsrpropdg  14160  aprval  14295  aprap  14299  lmfval  14916  lgsquadlem3  15807  wksfval  16172  trlsfvalg  16233  eupthsg  16295