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  7746  dmmulpq  7747  recmulnqg  7758  enq0enq  7798  ltrelxr  8386  ltxr  10177  shftidt2  11597  releqgg  14023  eqgex  14024  prdsex  14172  prdsval  14173  prdsbaslemss  14174  dvdsrzring  14938  lmfval  15294  lmbr  15314  cnmptid  15382  lgsquadlem3  16198  wksfval  16563