Theorem opabbidv 4198

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 1581	. 2 |- F/ x ph
2		nfv 1581	. 2 |- F/ y ph
3		opabbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
4	1, 2, 3	opabbid 4197	1 |- ( ph -> { <. x , y >. | ps } = { <. x , y >. | ch } )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   {copab 4192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-opab 4194

This theorem is used by:  opabbii  4199  csbopabg  4210  xpeq1  4790  xpeq2  4791  opabbi2dv  4931  csbcnvg  4966  resopab2  5113  mptcnv  5193  cores  5294  xpcom  5337  dffn5im  5751  f1oiso2  6036  f1ocnvd  6295  f1o3d  6301  ofreq  6309  f1od2  6475  shftfvalg  11604  shftfval  11607  2shfti  11617  releqgg  14081  eqgex  14082  eqgfval  14083  prdsex  14278  prdsval  14279  dvdsrvald  14508  dvdsrpropdg  14562  aprval  14699  aprap  14706  aprprop  14709  lmfval  15436  lgsquadlem3  16420  wksfval  16785  trlsfvalg  16846  eupthsg  16908