Theorem opabbii 5167

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 2737	. 2 ⊢ 𝑧 = 𝑧
2		opabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 11	. . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓))
4	3	opabbidv 5166	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1542  {copab 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-opab 5163

This theorem is referenced by:  mptv  5206  2rbropap  5520  dfid4  5528  fconstmpt  5694  xpundi  5701  xpundir  5702  inxpOLD  5789  csbcnv  5840  cnvco  5842  resopab  6001  opabresid  6017  cnvi  6107  cnvun  6108  cnvxp  6123  cnvcnv3  6154  coundi  6213  coundir  6214  mptun  6646  fvopab6  6984  fmptsng  7124  fmptsnd  7125  cbvoprab1  7455  cbvoprab12  7457  dmoprabss  7472  mpomptx  7481  resoprab  7486  elrnmpores  7506  ov6g  7532  1st2val  7971  2nd2val  7972  dfoprab3s  8007  dfoprab3  8008  dfoprab4  8009  opabn1stprc  8012  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  fsplit  8069  mapsncnv  8843  xpcomco  9007  marypha2lem2  9351  oemapso  9603  ttrclresv  9638  leweon  9933  r0weon  9934  compsscnv  10293  fpwwe  10569  ltrelxr  11205  ltxrlt  11215  ltxr  13041  shftidt2  15016  prdsle  17394  prdsless  17395  prdsleval  17409  dfiso2  17708  joindm  18308  meetdm  18322  gaorb  19248  efgcpbllema  19695  frgpuplem  19713  dvdsrzring  21428  pjfval2  21676  ltbval  22010  ltbwe  22011  opsrle  22014  opsrtoslem1  22022  opsrtoslem2  22023  lmfval  23188  lmbr  23214  lgsquadlem3  27361  perpln1  28794  outpasch  28839  ishpg  28843  axcontlem2  29050  wksfval  29695  wlkson  29740  pthsfval  29804  ispth  29806  dfadj2  31972  dmadjss  31974  cnvadj  31979  mpomptxf  32767  lsmsnorb2  33484  satfv0  35571  satfvsuclem1  35572  satfvsuclem2  35573  satfbrsuc  35579  satf0  35585  satf0suclem  35588  fmlasuc0  35597  dfsuccf2  36154  fneer  36566  bj-dfmpoa  37368  bj-mpomptALT  37369  bj-brab2a1  37401  bj-imdiridlem  37437  bj-opabco  37440  opropabco  37972  xpv  38510  cnvepres  38552  inxp2  38623  disjecxrn  38660  xrninxp  38663  xrninxp2  38664  rnxrnres  38670  rnxrncnvepres  38671  rnxrnidres  38672  blockadjliftmap  38706  dfsucmap3  38711  dfsucmap4  38713  dfcoss2  38751  dfcoss3  38752  cosscnv  38754  coss1cnvres  38755  coss2cnvepres  38756  1cossres  38767  dfcoels  38768  ressn2  38780  br1cosscnvxrn  38812  1cosscnvxrn  38813  coss0  38817  cossid  38818  dfssr2  38827  dfpetparts2  39220  dfpeters2  39222  petseq  39224  cmtfvalN  39583  cmtvalN  39584  cvrfval  39641  cvrval  39642  dicval2  41552  aks6d1c1p1rcl  42475  aks6d1c1rh  42492  fgraphopab  43557  fgraphxp  43558  modelaxreplem2  45332  mptssid  45596  dfnelbr2  47630  opabbrfex0d  47643  opabbrfexd  47645  upwlksfval  48492  xpsnopab  48514  mpomptx2  48692  upfval2  49533