Theorem opabbidv 4055

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   {copab 4049

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-opab 4051

This theorem is referenced by:  opabbii  4056  csbopabg  4067  xpeq1  4625  xpeq2  4626  opabbi2dv  4760  csbcnvg  4795  resopab2  4938  mptcnv  5013  cores  5114  xpcom  5157  dffn5im  5542  f1oiso2  5806  f1ocnvd  6051  ofreq  6064  f1od2  6214  shftfvalg  10782  shftfval  10785  2shfti  10795  lmfval  12986