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  5968  f1ocnvd  6225  ofreq  6239  f1od2  6400  shftfvalg  11396  shftfval  11399  2shfti  11409  prdsex  13370  prdsval  13374  releqgg  13825  eqgex  13826  eqgfval  13827  dvdsrvald  14126  dvdsrpropdg  14180  aprval  14315  aprap  14319  lmfval  14936  lgsquadlem3  15827  wksfval  16192  trlsfvalg  16253  eupthsg  16315