Theorem opabbii 4101

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 2196	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4100	. 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 4094

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-opab 4096

This theorem is referenced by:  mptv  4131  fconstmpt  4711  xpundi  4720  xpundir  4721  inxp  4801  cnvco  4852  resopab  4991  opabresid  5000  cnvi  5075  cnvun  5076  cnvin  5078  cnvxp  5089  cnvcnv3  5120  coundi  5172  coundir  5173  mptun  5392  fvopab6  5661  cbvoprab1  5998  cbvoprab12  6000  dmoprabss  6008  mpomptx  6017  resoprab  6022  ov6g  6065  dfoprab3s  6257  dfoprab3  6258  dfoprab4  6259  mapsncnv  6763  xpcomco  6894  dmaddpq  7463  dmmulpq  7464  recmulnqg  7475  enq0enq  7515  ltrelxr  8104  ltxr  9867  shftidt2  11014  prdsex  12971  prdsval  12975  prdsbaslemss  12976  releqgg  13426  eqgex  13427  dvdsrzring  14235  lmfval  14512  lmbr  14533  cnmptid  14601  lgsquadlem3  15404