Theorem opabbii 4071

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 4070	. 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 4064

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 4066

This theorem is referenced by:  mptv  4101  fconstmpt  4674  xpundi  4683  xpundir  4684  inxp  4762  cnvco  4813  resopab  4952  opabresid  4961  cnvi  5034  cnvun  5035  cnvin  5037  cnvxp  5048  cnvcnv3  5079  coundi  5131  coundir  5132  mptun  5348  fvopab6  5613  cbvoprab1  5947  cbvoprab12  5949  dmoprabss  5957  mpomptx  5966  resoprab  5971  ov6g  6012  dfoprab3s  6191  dfoprab3  6192  dfoprab4  6193  mapsncnv  6695  xpcomco  6826  dmaddpq  7378  dmmulpq  7379  recmulnqg  7390  enq0enq  7430  ltrelxr  8018  ltxr  9775  shftidt2  10841  prdsex  12718  releqgg  13080  dvdsrzring  13496  lmfval  13695  lmbr  13716  cnmptid  13784