Theorem opabbii 4199

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 2238	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4198	. 2 |- ( z = z -> { <. x , y >. | ph } = { <. x , y >. | ps } )
5	1, 4	ax-mp 5	1 |- { <. x , y >. | ph } = { <. x , y >. | ps }

This proof depends on syntax axioms:   <-> wb 105   = wceq 1402   {copab 4192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-opab 4194

This theorem is used by:  mptv  4230  fconstmpt  4824  xpundi  4833  xpundir  4834  inxp  4916  cnvco  4967  resopab  5110  opabresid  5119  cnvi  5195  cnvun  5196  cnvin  5198  cnvxp  5209  cnvcnv3  5240  coundi  5292  coundir  5293  mptun  5518  fvopab6  5808  cbvoprab1  6163  cbvoprab12  6165  dmoprabss  6173  mpomptx  6182  resoprab  6187  ov6g  6230  dfoprab3s  6428  dfoprab3  6429  dfoprab4  6430  opabn1stprc  6433  mapsncnv  6981  xpcomco  7128  dmaddpq  7752  dmmulpq  7753  recmulnqg  7764  enq0enq  7804  ltrelxr  8392  ltxr  10194  shftidt2  11619  releqgg  14082  eqgex  14083  prdsex  14279  prdsval  14280  prdsbaslemss  14281  dvdsrzring  15047  lmfval  15419  lmbr  15439  cnmptid  15507  lgsquadlem3  16403  wksfval  16768