Theorem opabbii 4097

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 2193	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4096	. 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 1364   {copab 4090

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-opab 4092

This theorem is referenced by:  mptv  4127  fconstmpt  4707  xpundi  4716  xpundir  4717  inxp  4797  cnvco  4848  resopab  4987  opabresid  4996  cnvi  5071  cnvun  5072  cnvin  5074  cnvxp  5085  cnvcnv3  5116  coundi  5168  coundir  5169  mptun  5386  fvopab6  5655  cbvoprab1  5991  cbvoprab12  5993  dmoprabss  6001  mpomptx  6010  resoprab  6015  ov6g  6058  dfoprab3s  6245  dfoprab3  6246  dfoprab4  6247  mapsncnv  6751  xpcomco  6882  dmaddpq  7441  dmmulpq  7442  recmulnqg  7453  enq0enq  7493  ltrelxr  8082  ltxr  9844  shftidt2  10979  prdsex  12883  releqgg  13293  eqgex  13294  dvdsrzring  14102  lmfval  14371  lmbr  14392  cnmptid  14460  lgsquadlem3  15236