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  11605  shftfval  11608  2shfti  11618  releqgg  14082  eqgex  14083  eqgfval  14084  prdsex  14279  prdsval  14280  dvdsrvald  14509  dvdsrpropdg  14563  aprval  14700  aprap  14707  aprprop  14710  lmfval  15419  lgsquadlem3  16403  wksfval  16768  trlsfvalg  16829  eupthsg  16891