Theorem opabbii 4516

Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)

Hypothesis

Ref	Expression
opabbii.1

Assertion

Ref	Expression
opabbii

Proof of Theorem opabbii

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2457	. 2
2		opabbii.1	. . . 4
3	2	a1i 11	. . 3
4	3	opabbidv 4515	. 2
5	1, 4	ax-mp 5	1

Syntax hints:  <->wb 184  =wceq 1395  {copab 4509

This theorem is referenced by:  mptv  4544  fconstmpt  5048  xpundi  5057  xpundir  5058  inxp  5140  csbcnv  5191  cnvco  5193  resopab  5325  opabresid  5332  cnvi  5415  cnvun  5416  cnvxp  5429  cnvcnv3  5461  coundi  5513  coundir  5514  mptun  5717  fvopab6  5980  fmptsng  6092  fmptsnd  6093  cbvoprab1  6369  cbvoprab12  6371  dmoprabss  6384  mpt2mptx  6393  resoprab  6398  elrnmpt2res  6416  ov6g  6440  1st2val  6826  2nd2val  6827  dfoprab3s  6855  dfoprab3  6856  dfoprab4  6857  fsplit  6905  mapsncnv  7485  xpcomco  7627  marypha2lem2  7916  oemapso  8122  leweon  8410  r0weon  8411  compsscnv  8772  fpwwe  9045  ltrelxr  9669  ltxrlt  9676  ltxr  11353  shftidt2  12914  prdsle  14859  prdsless  14860  prdsleval  14874  joindm  15633  meetdm  15647  gaorb  16345  efgcpbllema  16772  frgpuplem  16790  ltbval  18136  ltbwe  18137  opsrle  18140  opsrtoslem1  18148  opsrtoslem2  18149  dvdsrzring  18507  dvdsrz  18508  pjfval2  18740  lmfval  19733  lmbr  19759  cnmptid  20162  lgsquadlem3  23631  perpln1  24087  axcontlem2  24268  wlks  24519  trls  24538  dfconngra1  24671  dfadj2  26804  dmadjss  26806  cnvadj  26811  mpt2mptxf  27518  dfid4  29103  fneer  30171  opropabco  30214  fgraphopab  31170  fgraphxp  31171  xpsnopab  32453  dfiso2  32568  mpt2mptx2  32924  cmtfvalN  34935  cmtvalN  34936  cvrfval  34993  cvrval  34994  dicval2  36906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-opab 4511