Theorem opabbii 4110

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

Syntax hints:   ↔ wb 105   = wceq 1372  {copab 4103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-opab 4105

This theorem is referenced by:  mptv  4140  fconstmpt  4720  xpundi  4729  xpundir  4730  inxp  4810  cnvco  4861  resopab  5000  opabresid  5009  cnvi  5084  cnvun  5085  cnvin  5087  cnvxp  5098  cnvcnv3  5129  coundi  5181  coundir  5182  mptun  5401  fvopab6  5670  cbvoprab1  6007  cbvoprab12  6009  dmoprabss  6017  mpomptx  6026  resoprab  6031  ov6g  6074  dfoprab3s  6266  dfoprab3  6267  dfoprab4  6268  mapsncnv  6772  xpcomco  6903  dmaddpq  7474  dmmulpq  7475  recmulnqg  7486  enq0enq  7526  ltrelxr  8115  ltxr  9879  shftidt2  11062  prdsex  13019  prdsval  13023  prdsbaslemss  13024  releqgg  13474  eqgex  13475  dvdsrzring  14283  lmfval  14582  lmbr  14603  cnmptid  14671  lgsquadlem3  15474