Theorem opabbidv 2670

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction rule).

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

Proof of Theorem opabbidv

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (ph -> A.xph)
2		ax-17 971	. 2 |- (ph -> A.yph)
3		opabbidv.1	. 2 |- (ph -> (ps <-> ch))
4	1, 2, 3	opabbid 2669	1 |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956  {copab 2666

This theorem is referenced by:  opabbii 2671  xpeq1 3200  xpeq2 3201  coeq1 3281  coeq2 3282  resopab2 3398  rdgeq1 3934  rdgeq2 3935  omv 4151  oev 4153  en2d 4400  unfilem3 4550  seq1val 6312  shftfval 6342  2shft 6352  icoshftf1olem 6410  geolim 7237  geolim1 7239  divccncf 7280  efcltlem2 7305  efseq1ex 7306  eftlext 7378  ef1tlub 7382  ef01tlub 7386  absef01tlub 7388  ef4pt 7400  ntrfval 7667  clsfval 7668  neifval 7714  lpfval 7742  cnpfval 7757  lmfval 7925  metcn4i 7972  opr1cn 7978  opr2cn 7979  fsumcnlem 7989  bcthlem15 8013  grpinvfval 8066  grplactfval 8096  ip1cnilem5 8377  nmofval 8425  ajfval 8469  htthlem3 8622  htthlem5 8624  occllem5 9177  pjmvalt 9238  hosmvalt 9511  hommvalt 9512  hodmvalt 9513  hfsmvalt 9514  hfmmvalt 9515  eigvalvalt 9823  bravalt 9867  brafnmult 9875  kbvalt 9876  kbmult 9879  kbass2t 10050  kbass5t 10053  cayleylem2 10410  rcfpfil 10597  rcfpfilOLD 10598  sfvlim 10605  sfvlimOLD 10606

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-opab 2667

Copyright terms: Public domain