Theorem opabbii 3953

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 2113	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 9	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 3952	. 2 |- ( z = z -> { <. x , y >. | ph } = { <. x , y >. | ps } )
5	1, 4	ax-mp 7	1 |- { <. x , y >. | ph } = { <. x , y >. | ps }

Syntax hints:   <-> wb 104   = wceq 1312   {copab 3946

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-opab 3948

This theorem is referenced by:  mptv  3983  fconstmpt  4544  xpundi  4553  xpundir  4554  inxp  4631  cnvco  4682  resopab  4819  opabresid  4828  cnvi  4899  cnvun  4900  cnvin  4902  cnvxp  4913  cnvcnv3  4944  coundi  4996  coundir  4997  mptun  5210  fvopab6  5469  cbvoprab1  5795  cbvoprab12  5797  dmoprabss  5805  mpomptx  5814  resoprab  5819  ov6g  5860  dfoprab3s  6039  dfoprab3  6040  dfoprab4  6041  mapsncnv  6540  xpcomco  6670  dmaddpq  7128  dmmulpq  7129  recmulnqg  7140  enq0enq  7180  ltrelxr  7742  ltxr  9448  shftidt2  10490  lmfval  12197  lmbr  12217  cnmptid  12285