Theorem opabbii 4072

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 2177	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4071	. 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 1353   {copab 4065

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-opab 4067

This theorem is referenced by:  mptv  4102  fconstmpt  4675  xpundi  4684  xpundir  4685  inxp  4763  cnvco  4814  resopab  4953  opabresid  4962  cnvi  5035  cnvun  5036  cnvin  5038  cnvxp  5049  cnvcnv3  5080  coundi  5132  coundir  5133  mptun  5349  fvopab6  5615  cbvoprab1  5950  cbvoprab12  5952  dmoprabss  5960  mpomptx  5969  resoprab  5974  ov6g  6015  dfoprab3s  6194  dfoprab3  6195  dfoprab4  6196  mapsncnv  6698  xpcomco  6829  dmaddpq  7381  dmmulpq  7382  recmulnqg  7393  enq0enq  7433  ltrelxr  8021  ltxr  9778  shftidt2  10844  prdsex  12724  releqgg  13086  dvdsrzring  13633  lmfval  13832  lmbr  13853  cnmptid  13921