Theorem opabbii 5179

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

Syntax hints:   ↔ wb 209   = wceq 1570  {copab 5174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-opab 5175

This theorem is referenced by:  mptv  5218  2rbropap  5551  dfid4  5559  fconstmpt  5725  xpundi  5732  xpundir  5733  cnvi  5873  csbcnv  5874  csbcnvOLD  5875  cnvco  5877  resopab  6038  opabresid  6054  cnvun  6141  cnvxp  6156  cnvcnv3  6188  coundi  6250  coundir  6251  mptun  6683  fvopab6  7026  fmptsng  7168  fmptsnd  7169  cbvoprab1  7499  cbvoprab12  7501  dmoprabss  7516  mpomptx  7525  resoprab  7530  elrnmpores  7550  ov6g  7576  1st2val  8015  2nd2val  8016  dfoprab3s  8051  dfoprab3  8052  dfoprab4  8053  opabn1stprc  8056  mptmpoopabbrd  8079  fsplit  8113  mapsncnv  8892  xpcomco  9056  marypha2lem2  9397  oemapso  9652  ttrclresv  9687  leweon  9996  r0weon  9997  compsscnv  10356  fpwwe  10632  ltrelxr  11271  ltxrlt  11281  ltxr  13141  shftidt2  15120  prdsle  17516  prdsless  17517  prdsleval  17531  dfiso2  17830  joindm  18430  meetdm  18444  gaorb  19378  efgcpbllema  19825  frgpuplem  19843  dvdsrzring  21592  pjfval2  21840  ltbval  22175  ltbwe  22176  opsrle  22179  opsrtoslem1  22187  opsrtoslem2  22188  lmfval  23370  lmbr  23396  lgsquadlem3  27527  perpln1  28971  outpasch  29018  ishpg  29022  tgaltai  29198  axcontlem2  29296  wksfval  29940  wlkson  29985  pthsfval  30049  ispth  30051  dfadj2  32218  dmadjss  32220  cnvadj  32225  mpomptxf  33004  lsmsnorb2  33686  satfv0  35831  satfvsuclem1  35832  satfvsuclem2  35833  satfbrsuc  35839  satf0  35845  satf0suclem  35848  fmlasuc0  35857  dfsuccf2  36414  fneer  36845  bj-dfmpoa  37741  bj-mpomptALT  37742  bj-brab2a1  37774  bj-imdiridlem  37810  bj-opabco  37813  opropabco  38356  xpv  38892  cnvepres  38934  inxp2  39005  disjecxrn  39042  xrninxp  39045  xrninxp2  39046  rnxrnres  39052  rnxrncnvepres  39053  rnxrnidres  39054  blockadjliftmap  39088  dfsucmap3  39093  dfsucmap4  39095  dfcoss2  39133  dfcoss3  39134  cosscnv  39136  coss1cnvres  39137  coss2cnvepres  39138  1cossres  39149  dfcoels  39150  ressn2  39162  br1cosscnvxrn  39194  1cosscnvxrn  39195  coss0  39199  cossid  39200  dfssr2  39209  dfpetparts2  39602  dfpeters2  39604  petseq  39606  cmtfvalN  39965  cmtvalN  39966  cvrfval  40023  cvrval  40024  dicval2  41934  aks6d1c1p1rcl  42856  aks6d1c1rh  42873  fgraphopab  43913  fgraphxp  43914  modelaxreplem2  45671  mptssid  45939  dfnelbr2  47993  opabbrfex0d  48006  opabbrfexd  48008  upwlksfval  48883  xpsnopab  48905  mpomptx2  49098  upfval2  49938