Theorem opabbii 4627

Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)

Hypothesis

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

Assertion

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

Proof of Theorem opabbii

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2353	. 2 |- z = z
2		opabbii.1	. . . 4 |- (ph <-> ps)
3	2	a1i 10	. . 3 |- (z = z -> (ph <-> ps))
4	3	opabbidv 4626	. 2 |- (z = z -> {<.x, y>. | ph} = {<.x, y>. | ps})
5	1, 4	ax-mp 5	1 |- {<.x, y>. | ph} = {<.x, y>. | ps}

Syntax hints:   <-> wb 176   = wceq 1642  {copab 4623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-opab 4624

This theorem is referenced by:  df1st2  4739  dfsset2  4744  dfco1  4749  dfsi2  4752  fconstopab  4816  xpundi  4833  xpundir  4834  inxp  4864  opabbi2i  4867  cnvco  4895  resopab  5000  opabresid  5004  cnvi  5033  cnvun  5034  cnvxp  5044  coundi  5083  coundir  5084  df2nd2  5112  fvopabg  5392  cbvoprab1  5568  cbvoprab12  5570  dmoprabss  5576  resoprab  5582  fnov  5592  ov6g  5601  mpt2mptx  5709  mptv  5719  scancan  6332