Theorem opabbii 5162

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 5161	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1541  {copab 5157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-opab 5158

This theorem is referenced by:  mptv  5201  2rbropap  5509  dfid4  5517  fconstmpt  5683  xpundi  5690  xpundir  5691  inxpOLD  5778  csbcnv  5829  cnvco  5831  resopab  5990  opabresid  6006  cnvi  6096  cnvun  6097  cnvxp  6112  cnvcnv3  6143  coundi  6202  coundir  6203  mptun  6635  fvopab6  6972  fmptsng  7111  fmptsnd  7112  cbvoprab1  7442  cbvoprab12  7444  dmoprabss  7459  mpomptx  7468  resoprab  7473  elrnmpores  7493  ov6g  7519  1st2val  7958  2nd2val  7959  dfoprab3s  7994  dfoprab3  7995  dfoprab4  7996  opabn1stprc  7999  mptmpoopabbrd  8021  mptmpoopabbrdOLD  8022  fsplit  8056  mapsncnv  8827  xpcomco  8991  marypha2lem2  9331  oemapso  9583  ttrclresv  9618  leweon  9913  r0weon  9914  compsscnv  10273  fpwwe  10548  ltrelxr  11184  ltxrlt  11194  ltxr  13020  shftidt2  14995  prdsle  17373  prdsless  17374  prdsleval  17388  dfiso2  17687  joindm  18287  meetdm  18301  gaorb  19227  efgcpbllema  19674  frgpuplem  19692  dvdsrzring  21407  pjfval2  21655  ltbval  21989  ltbwe  21990  opsrle  21993  opsrtoslem1  22001  opsrtoslem2  22002  lmfval  23167  lmbr  23193  lgsquadlem3  27340  perpln1  28708  outpasch  28753  ishpg  28757  axcontlem2  28964  wksfval  29609  wlkson  29654  pthsfval  29718  ispth  29720  dfadj2  31886  dmadjss  31888  cnvadj  31893  mpomptxf  32683  lsmsnorb2  33401  satfv0  35474  satfvsuclem1  35475  satfvsuclem2  35476  satfbrsuc  35482  satf0  35488  satf0suclem  35491  fmlasuc0  35500  dfsuccf2  36057  fneer  36469  bj-dfmpoa  37235  bj-mpomptALT  37236  bj-brab2a1  37266  bj-imdiridlem  37302  bj-opabco  37305  opropabco  37837  cnvepres  38409  inxp2  38472  disjecxrn  38509  xrninxp  38512  xrninxp2  38513  rnxrnres  38519  rnxrncnvepres  38520  rnxrnidres  38521  blockadjliftmap  38545  dfsucmap3  38549  dfsucmap4  38551  dfcoss2  38588  dfcoss3  38589  cosscnv  38591  coss1cnvres  38592  coss2cnvepres  38593  1cossres  38604  dfcoels  38605  ressn2  38617  br1cosscnvxrn  38649  1cosscnvxrn  38650  coss0  38654  cossid  38655  dfssr2  38664  dfblockliftfix2  38809  cmtfvalN  39382  cmtvalN  39383  cvrfval  39440  cvrval  39441  dicval2  41351  aks6d1c1p1rcl  42274  aks6d1c1rh  42291  fgraphopab  43360  fgraphxp  43361  modelaxreplem2  45136  mptssid  45401  dfnelbr2  47435  opabbrfex0d  47448  opabbrfexd  47450  upwlksfval  48297  xpsnopab  48319  mpomptx2  48497  upfval2  49338