Theorem opabbidv 2675

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 973	. 2 |- (ph -> A.xph)
2		ax-17 973	. 2 |- (ph -> A.yph)
3		opabbidv.1	. 2 |- (ph -> (ps <-> ch))
4	1, 2, 3	opabbid 2674	1 |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958  {copab 2671

This theorem is referenced by:  opabbii 2676  xpeq1 3206  xpeq2 3207  coeq1 3287  coeq2 3288  resopab2 3404  rdgeq1 3940  rdgeq2 3941  omv 4157  oev 4159  en2d 4406  unfilem3 4562  seq1val 6313  shftfval 6343  2shft 6353  icoshftf1olem 6411  geolim 7237  geolim1 7239  divccncf 7280  efcltlem2 7305  efseq1ex 7306  eftlext 7378  ef1tlub 7382  ef01tlub 7386  absef01tlub 7388  ef4pt 7400  ntrfval 7664  clsfval 7665  neifval 7711  lpfval 7739  cnpfval 7754  lmfval 7922  metcn4i 7969  opr1cn 7975  opr2cn 7976  fsumcnlem 7986  bcthlem15 8010  grpinvfval 8062  grplactfval 8092  ip1cnilem5 8373  nmofval 8421  ajfval 8465  htthlem3 8618  htthlem5 8620  occllem5 9172  pjmvalt 9233  hosmvalt 9506  hommvalt 9507  hodmvalt 9508  hfsmvalt 9509  hfmmvalt 9510  eigvalvalt 9818  bravalt 9862  brafnmult 9870  kbvalt 9871  kbmult 9874  kbass2t 10045  kbass5t 10048  cayleylem2 10405  rcfpfil 10569  sfvlim 10576  sfvlimOLD 10577

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-opab 2672

Copyright terms: Public domain