Theorem opabbii 5172

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  {copab 5167

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-opab 5168

This theorem is used by:  mptv  5211  2rbropap  5539  dfid4  5547  fconstmpt  5713  xpundi  5720  xpundir  5721  cnvi  5863  csbcnv  5864  csbcnvOLD  5865  cnvco  5867  resopab  6026  opabresid  6042  cnvun  6133  cnvxpOLD  6148  cnvcnv3  6180  coundi  6247  coundir  6248  mptun  6683  fvopab6  7026  fmptsng  7171  fmptsnd  7172  cbvoprab1  7505  cbvoprab12  7507  dmoprabss  7522  mpomptx  7531  resoprab  7536  elrnmpores  7556  ov6g  7582  mpt3mpt  7683  mpt3fvd  7686  1st2val  8027  2nd2val  8028  dfoprab3s  8062  dfoprab3  8063  dfoprab4  8064  opabn1stprc  8067  mptmpoopabbrd  8092  fsplit  8126  mapsncnv  8914  xpcomco  9079  marypha2lem2  9421  oemapso  9676  ttrclresv  9711  leweon  10083  r0weon  10084  compsscnv  10442  fpwwe  10724  ltrelxr  11363  ltxrlt  11373  ltxr  13237  shftidt2  15227  prdsle  17626  prdsless  17627  prdsleval  17641  dfiso2  17940  joindm  18540  meetdm  18554  gaorb  19514  efgcpbllema  19961  frgpuplem  19979  dvdsrzring  21760  pjfval2  22008  ltbval  22345  ltbwe  22346  opsrle  22349  opsrtoslem1  22357  opsrtoslem2  22358  lmfval  23543  lmbr  23569  lgsquadlem3  27702  perpln1  29178  outpasch  29226  ishpg  29230  tgaaddcpbllem2  29343  tgaaddcpbllem3  29344  tgaltai  29438  axcontlem2  29536  wksfval  30183  wlkson  30228  pthsfval  30297  ispth  30299  dfadj2  32480  dmadjss  32482  cnvadj  32487  mpomptxf  33265  lsmsnorb2  33940  satfv0  36102  satfvsuclem1  36103  satfvsuclem2  36104  satfbrsuc  36110  satf0  36116  satf0suclem  36119  fmlasuc0  36128  dfsuccf2  36685  fneer  37121  bj-dfmpoa  38019  bj-mpomptALT  38020  bj-brab2a1  38050  bj-imdiridlem  38086  bj-opabco  38089  opropabco  38638  xpv  39174  cnvepres  39216  inxp2  39287  disjecxrn  39324  xrninxp  39327  xrninxp2  39328  rnxrnres  39334  rnxrncnvepres  39335  rnxrnidres  39336  blockadjliftmap  39370  dfsucmap3  39375  dfsucmap4  39377  dfcoss2  39415  dfcoss3  39416  cosscnv  39418  coss1cnvres  39419  coss2cnvepres  39420  1cossres  39431  dfcoels  39432  ressn2  39444  br1cosscnvxrn  39476  1cosscnvxrn  39477  coss0  39481  cossid  39482  dfssr2  39491  dfpetparts2  39884  dfpeters2  39886  petseq  39888  cmtfvalN  40247  cmtvalN  40248  cvrfval  40305  cvrval  40306  dicval2  42216  aks6d1c1p1rcl  43138  aks6d1c1rh  43155  fgraphopab  44189  fgraphxp  44190  modelaxreplem2  45947  mptssid  46222  dfnelbr2  48312  opabbrfex0d  48325  opabbrfexd  48327  upwlksfval  49202  xpsnopab  49224  mpomptx2  49416  upfval2  50254