Theorem biopabi 2103

Description: Equivalent wff's yield equal class abstractions.

Hypothesis

Ref	Expression
biopab.1	|- (ph <-> ps)

Assertion

Ref	Expression
biopabi	|- {<.x, y>. | ph} = {<.x, y>. | ps}

Distinct variable group(s):   x,y

Proof of Theorem biopabi

Step	Hyp	Ref	Expression
1		cleqid 1102	. 2 |- z = z
2		biopab.1	. . . 4 |- (ph <-> ps)
3	2	a1i 7	. . 3 |- (z = z -> (ph <-> ps))
4	3	biopabdv 2102	. 2 |- (z = z -> {<.x, y>. | ph} = {<.x, y>. | ps})
5	1, 4	ax-mp 6	1 |- {<.x, y>. | ph} = {<.x, y>. | ps}

Syntax hints:   <-> wb 127   = weq 797   = wceq 1091  {copab 2055

This theorem is referenced by:  fconstopab 2448  xpundi 2461  xpundir 2462  cnvco 2520  resopab 2598  fvopabg 2872  abrexexlem2 2911  dmoprabss 3032  fnoprab 3038  fnoprval 3042  fo1st 3094  fo2nd 3095  1st2val 3097  genpdm 3899  sqrval 4729  ocvalt 5161  dfchsup2 5299  spanvalt 5300  hsupval2t 5301

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-opab 2098

metamath.org