Theorem opabbii 4198

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 4197	. 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 4191

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 4193

This theorem is used by:  mptv  4228  fconstmpt  4822  xpundi  4831  xpundir  4832  inxp  4914  cnvco  4965  resopab  5107  opabresid  5116  cnvi  5192  cnvun  5193  cnvin  5195  cnvxp  5206  cnvcnv3  5237  coundi  5289  coundir  5290  mptun  5515  fvopab6  5805  cbvoprab1  6160  cbvoprab12  6162  dmoprabss  6170  mpomptx  6179  resoprab  6184  ov6g  6227  dfoprab3s  6424  dfoprab3  6425  dfoprab4  6426  opabn1stprc  6429  mapsncnv  6977  xpcomco  7124  dmaddpq  7747  dmmulpq  7748  recmulnqg  7759  enq0enq  7799  ltrelxr  8387  ltxr  10188  shftidt2  11613  releqgg  14076  eqgex  14077  prdsex  14256  prdsval  14257  prdsbaslemss  14258  dvdsrzring  15022  lmfval  15385  lmbr  15405  cnmptid  15473  lgsquadlem3  16364  wksfval  16729