Theorem opabbii 4111

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 2205	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4110	. 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 1373   {copab 4104

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-opab 4106

This theorem is referenced by:  mptv  4141  fconstmpt  4722  xpundi  4731  xpundir  4732  inxp  4812  cnvco  4863  resopab  5003  opabresid  5012  cnvi  5087  cnvun  5088  cnvin  5090  cnvxp  5101  cnvcnv3  5132  coundi  5184  coundir  5185  mptun  5407  fvopab6  5676  cbvoprab1  6017  cbvoprab12  6019  dmoprabss  6027  mpomptx  6036  resoprab  6041  ov6g  6084  dfoprab3s  6276  dfoprab3  6277  dfoprab4  6278  mapsncnv  6782  xpcomco  6921  dmaddpq  7492  dmmulpq  7493  recmulnqg  7504  enq0enq  7544  ltrelxr  8133  ltxr  9897  shftidt2  11143  prdsex  13101  prdsval  13105  prdsbaslemss  13106  releqgg  13556  eqgex  13557  dvdsrzring  14365  lmfval  14664  lmbr  14685  cnmptid  14753  lgsquadlem3  15556