Theorem opabbii 5215

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

Syntax hints:   ↔ wb 205   = wceq 1542  {copab 5210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-opab 5211

This theorem is referenced by:  mptv  5264  2rbropap  5566  dfid4  5575  fconstmpt  5737  xpundi  5743  xpundir  5744  inxp  5831  csbcnv  5882  cnvco  5884  resopab  6033  opabresid  6048  cnvi  6139  cnvun  6140  cnvxp  6154  cnvcnv3  6185  coundi  6244  coundir  6245  mptun  6694  fvopab6  7029  fmptsng  7163  fmptsnd  7164  cbvoprab1  7493  cbvoprab12  7495  dmoprabss  7508  mpomptx  7518  resoprab  7523  elrnmpores  7543  ov6g  7568  1st2val  8000  2nd2val  8001  dfoprab3s  8036  dfoprab3  8037  dfoprab4  8038  opabn1stprc  8041  mptmpoopabbrd  8064  mptmpoopabbrdOLD  8066  fsplit  8100  mapsncnv  8884  xpcomco  9059  marypha2lem2  9428  oemapso  9674  ttrclresv  9709  leweon  10003  r0weon  10004  compsscnv  10363  fpwwe  10638  ltrelxr  11272  ltxrlt  11281  ltxr  13092  shftidt2  15025  prdsle  17405  prdsless  17406  prdsleval  17420  dfiso2  17716  joindm  18325  meetdm  18339  gaorb  19166  efgcpbllema  19617  frgpuplem  19635  dvdsrzring  21023  pjfval2  21256  ltbval  21590  ltbwe  21591  opsrle  21594  opsrtoslem1  21608  opsrtoslem2  21609  lmfval  22728  lmbr  22754  lgsquadlem3  26875  perpln1  27951  outpasch  27996  ishpg  28000  axcontlem2  28213  wksfval  28856  wlkson  28903  pthsfval  28968  ispth  28970  dfadj2  31126  dmadjss  31128  cnvadj  31133  mpomptxf  31893  lsmsnorb2  32491  satfv0  34338  satfvsuclem1  34339  satfvsuclem2  34340  satfbrsuc  34346  satf0  34352  satf0suclem  34355  fmlasuc0  34364  fneer  35227  bj-dfmpoa  35988  bj-mpomptALT  35989  bj-brab2a1  36019  bj-imdiridlem  36055  bj-opabco  36058  opropabco  36581  cnvepres  37156  inxp2  37225  disjecxrn  37248  xrninxp  37251  xrninxp2  37252  rnxrnres  37258  rnxrncnvepres  37259  rnxrnidres  37260  dfcoss2  37272  dfcoss3  37273  cosscnv  37275  coss1cnvres  37276  coss2cnvepres  37277  1cossres  37288  dfcoels  37289  ressn2  37301  br1cosscnvxrn  37333  1cosscnvxrn  37334  coss0  37338  cossid  37339  dfssr2  37358  cmtfvalN  38069  cmtvalN  38070  cvrfval  38127  cvrval  38128  dicval2  40039  fgraphopab  41938  fgraphxp  41939  mptssid  43930  dfnelbr2  45968  opabbrfex0d  45981  opabbrfexd  45983  upwlksfval  46500  xpsnopab  46522  mpomptx2  46964