Theorem opabbidv 4030

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1335   {copab 4024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-opab 4026

This theorem is referenced by:  opabbii  4031  csbopabg  4042  xpeq1  4599  xpeq2  4600  opabbi2dv  4734  csbcnvg  4769  resopab2  4912  mptcnv  4987  cores  5088  xpcom  5131  dffn5im  5513  f1oiso2  5774  f1ocnvd  6019  ofreq  6032  f1od2  6179  shftfvalg  10711  shftfval  10714  2shfti  10724  lmfval  12563