Theorem opabbii 5171

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  {copab 5166

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-opab 5167

This theorem is used by:  mptv  5210  2rbropap  5538  dfid4  5546  fconstmpt  5712  xpundi  5719  xpundir  5720  cnvi  5862  csbcnv  5863  csbcnvOLD  5864  cnvco  5866  resopab  6025  opabresid  6041  cnvun  6132  cnvxpOLD  6147  cnvcnv3  6179  coundi  6248  coundir  6249  mptun  6686  fvopab6  7029  fmptsng  7174  fmptsnd  7175  cbvoprab1  7508  cbvoprab12  7510  dmoprabss  7525  mpomptx  7534  resoprab  7539  elrnmpores  7559  ov6g  7585  mpt3mpt  7686  mpt3fvd  7689  1st2val  8030  2nd2val  8031  dfoprab3s  8065  dfoprab3  8066  dfoprab4  8067  opabn1stprc  8070  mptmpoopabbrd  8095  fsplit  8131  mapsncnv  8925  xpcomco  9090  marypha2lem2  9432  oemapso  9687  ttrclresv  9722  leweon  10094  r0weon  10095  compsscnv  10453  fpwwe  10735  ltrelxr  11374  ltxrlt  11384  ltxr  13248  shftidt2  15240  prdsle  17639  prdsless  17640  prdsleval  17654  dfiso2  17953  joindm  18553  meetdm  18567  gaorb  19527  efgcpbllema  19974  frgpuplem  19992  dvdsrzring  21773  pjfval2  22021  ltbval  22358  ltbwe  22359  opsrle  22362  opsrtoslem1  22370  opsrtoslem2  22371  lmfval  23556  lmbr  23582  lgsquadlem3  27715  perpln1  29191  outpasch  29239  ishpg  29243  tgaaddcpbllem2  29356  tgaaddcpbllem3  29357  tgaltai  29451  axcontlem2  29549  wksfval  30196  wlkson  30241  pthsfval  30310  ispth  30312  dfadj2  32493  dmadjss  32495  cnvadj  32500  mpomptxf  33320  lsmsnorb2  33994  onf1we  35772  werankwe  35792  werankwe2  35793  dmr0ss  35942  satfv0  36210  satfvsuclem1  36211  satfvsuclem2  36212  satfbrsuc  36218  satf0  36224  satf0suclem  36227  fmlasuc0  36236  dfsuccf2  36798  fneer  37234  bj-dfmpoa  38133  bj-mpomptALT  38134  bj-brab2a1  38164  bj-imdiridlem  38200  bj-opabco  38203  opropabco  38752  xpv  39288  cnvepres  39330  inxp2  39401  disjecxrn  39438  xrninxp  39441  xrninxp2  39442  rnxrnres  39448  rnxrncnvepres  39449  rnxrnidres  39450  blockadjliftmap  39484  dfsucmap3  39489  dfsucmap4  39491  dfcoss2  39529  dfcoss3  39530  cosscnv  39532  coss1cnvres  39533  coss2cnvepres  39534  1cossres  39545  dfcoels  39546  ressn2  39558  br1cosscnvxrn  39590  1cosscnvxrn  39591  coss0  39595  cossid  39596  dfssr2  39605  dfpetparts2  39998  dfpeters2  40000  petseq  40002  cmtfvalN  40361  cmtvalN  40362  cvrfval  40419  cvrval  40420  dicval2  42330  aks6d1c1p1rcl  43252  aks6d1c1rh  43269  fgraphopab  44299  fgraphxp  44300  modelaxreplem2  46063  mptssid  46347  dfnelbr2  48437  opabbrfex0d  48450  opabbrfexd  48452  upwlksfval  49327  xpsnopab  49349  mpomptx2  49541  upfval2  50387