Theorem opabbii 4179

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 2234	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4178	. 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 1398   {copab 4172

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-opab 4174

This theorem is referenced by:  mptv  4209  fconstmpt  4799  xpundi  4808  xpundir  4809  inxp  4891  cnvco  4942  resopab  5084  opabresid  5093  cnvi  5169  cnvun  5170  cnvin  5172  cnvxp  5183  cnvcnv3  5214  coundi  5266  coundir  5267  mptun  5492  fvopab6  5776  cbvoprab1  6127  cbvoprab12  6129  dmoprabss  6137  mpomptx  6146  resoprab  6151  ov6g  6194  dfoprab3s  6386  dfoprab3  6387  dfoprab4  6388  opabn1stprc  6391  mapsncnv  6932  xpcomco  7079  dmaddpq  7696  dmmulpq  7697  recmulnqg  7708  enq0enq  7748  ltrelxr  8336  ltxr  10111  shftidt2  11521  prdsex  13499  prdsval  13503  prdsbaslemss  13504  releqgg  13954  eqgex  13955  dvdsrzring  14768  lmfval  15075  lmbr  15095  cnmptid  15163  lgsquadlem3  15969  wksfval  16334