Theorem opabbii 4431

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 2382	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 11	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4430	. 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 184   = wceq 1399   {copab 4424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-opab 4426

This theorem is referenced by:  mptv  4459  fconstmpt  4957  xpundi  4966  xpundir  4967  inxp  5048  csbcnv  5099  cnvco  5101  resopab  5232  opabresid  5239  cnvi  5320  cnvun  5321  cnvxp  5334  cnvcnv3  5365  coundi  5416  coundir  5417  mptun  5620  fvopab6  5882  fmptsng  5994  fmptsnd  5995  cbvoprab1  6268  cbvoprab12  6270  dmoprabss  6283  mpt2mptx  6292  resoprab  6297  elrnmpt2res  6315  ov6g  6339  1st2val  6725  2nd2val  6726  dfoprab3s  6754  dfoprab3  6755  dfoprab4  6756  fsplit  6804  mapsncnv  7384  xpcomco  7526  marypha2lem2  7811  oemapso  8014  leweon  8302  r0weon  8303  compsscnv  8664  fpwwe  8935  ltrelxr  9559  ltxrlt  9566  ltxr  11245  shftidt2  12916  prdsle  14869  prdsless  14870  prdsleval  14884  dfiso2  15178  joindm  15750  meetdm  15764  gaorb  16462  efgcpbllema  16889  frgpuplem  16907  ltbval  18249  ltbwe  18250  opsrle  18253  opsrtoslem1  18261  opsrtoslem2  18262  dvdsrzring  18614  pjfval2  18831  lmfval  19819  lmbr  19845  cnmptid  20247  lgsquadlem3  23748  perpln1  24207  axcontlem2  24389  wlks  24640  trls  24659  dfconngra1  24792  dfadj2  26920  dmadjss  26922  cnvadj  26927  mpt2mptxf  27665  dfid4  29269  fneer  30337  opropabco  30380  fgraphopab  31338  fgraphxp  31339  xpsnopab  32771  mpt2mptx2  33124  cmtfvalN  35348  cmtvalN  35349  cvrfval  35406  cvrval  35407  dicval2  37319