Theorem opabbii 4156

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 2231	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4155	. 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 105   = wceq 1397   {copab 4149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-opab 4151

This theorem is referenced by:  mptv  4186  fconstmpt  4773  xpundi  4782  xpundir  4783  inxp  4864  cnvco  4915  resopab  5057  opabresid  5066  cnvi  5141  cnvun  5142  cnvin  5144  cnvxp  5155  cnvcnv3  5186  coundi  5238  coundir  5239  mptun  5464  fvopab6  5743  cbvoprab1  6093  cbvoprab12  6095  dmoprabss  6103  mpomptx  6112  resoprab  6117  ov6g  6160  dfoprab3s  6353  dfoprab3  6354  dfoprab4  6355  opabn1stprc  6358  mapsncnv  6864  xpcomco  7010  dmaddpq  7599  dmmulpq  7600  recmulnqg  7611  enq0enq  7651  ltrelxr  8240  ltxr  10010  shftidt2  11410  prdsex  13370  prdsval  13374  prdsbaslemss  13375  releqgg  13825  eqgex  13826  dvdsrzring  14636  lmfval  14936  lmbr  14956  cnmptid  15024  lgsquadlem3  15827  wksfval  16192