Theorem opabbii 5139

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

Syntax hints:   ↔ wb 207   = wceq 1547  {copab 5134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-opab 5135

This theorem is referenced by:  mptv  5178  2rbropap  5506  dfid4  5514  fconstmpt  5680  xpundi  5687  xpundir  5688  csbcnv  5825  cnvco  5827  resopab  5986  opabresid  6002  cnvi  6092  cnvun  6093  cnvxp  6108  cnvcnv3  6139  coundi  6198  coundir  6199  mptun  6631  fvopab6  6970  fmptsng  7112  fmptsnd  7113  cbvoprab1  7443  cbvoprab12  7445  dmoprabss  7460  mpomptx  7469  resoprab  7474  elrnmpores  7494  ov6g  7520  1st2val  7959  2nd2val  7960  dfoprab3s  7995  dfoprab3  7996  dfoprab4  7997  opabn1stprc  8000  mptmpoopabbrd  8022  fsplit  8056  mapsncnv  8831  xpcomco  8995  marypha2lem2  9339  oemapso  9594  ttrclresv  9629  leweon  9924  r0weon  9925  compsscnv  10284  fpwwe  10560  ltrelxr  11197  ltxrlt  11207  ltxr  13057  shftidt2  15034  prdsle  17416  prdsless  17417  prdsleval  17431  dfiso2  17730  joindm  18330  meetdm  18344  gaorb  19273  efgcpbllema  19720  frgpuplem  19738  dvdsrzring  21436  pjfval2  21684  ltbval  22019  ltbwe  22020  opsrle  22023  opsrtoslem1  22031  opsrtoslem2  22032  lmfval  23215  lmbr  23241  lgsquadlem3  27363  perpln1  28796  outpasch  28841  ishpg  28845  axcontlem2  29052  wksfval  29696  wlkson  29741  pthsfval  29805  ispth  29807  dfadj2  31974  dmadjss  31976  cnvadj  31981  mpomptxf  32770  lsmsnorb2  33475  satfv0  35586  satfvsuclem1  35587  satfvsuclem2  35588  satfbrsuc  35594  satf0  35600  satf0suclem  35603  fmlasuc0  35612  dfsuccf2  36169  fneer  36581  bj-dfmpoa  37476  bj-mpomptALT  37477  bj-brab2a1  37509  bj-imdiridlem  37545  bj-opabco  37548  opropabco  38091  xpv  38629  cnvepres  38671  inxp2  38742  disjecxrn  38779  xrninxp  38782  xrninxp2  38783  rnxrnres  38789  rnxrncnvepres  38790  rnxrnidres  38791  blockadjliftmap  38825  dfsucmap3  38830  dfsucmap4  38832  dfcoss2  38870  dfcoss3  38871  cosscnv  38873  coss1cnvres  38874  coss2cnvepres  38875  1cossres  38886  dfcoels  38887  ressn2  38899  br1cosscnvxrn  38931  1cosscnvxrn  38932  coss0  38936  cossid  38937  dfssr2  38946  dfpetparts2  39339  dfpeters2  39341  petseq  39343  cmtfvalN  39702  cmtvalN  39703  cvrfval  39760  cvrval  39761  dicval2  41671  aks6d1c1p1rcl  42593  aks6d1c1rh  42610  fgraphopab  43648  fgraphxp  43649  modelaxreplem2  45423  mptssid  45685  dfnelbr2  47736  opabbrfex0d  47749  opabbrfexd  47751  upwlksfval  48626  xpsnopab  48648  mpomptx2  48826  upfval2  49667