Theorem opabbii 4182

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

Syntax hints:   ↔ wb 105   = wceq 1398  {copab 4175

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-opab 4177

This theorem is referenced by:  mptv  4212  fconstmpt  4802  xpundi  4811  xpundir  4812  inxp  4894  cnvco  4945  resopab  5087  opabresid  5096  cnvi  5172  cnvun  5173  cnvin  5175  cnvxp  5186  cnvcnv3  5217  coundi  5269  coundir  5270  mptun  5495  fvopab6  5779  cbvoprab1  6133  cbvoprab12  6135  dmoprabss  6143  mpomptx  6152  resoprab  6157  ov6g  6200  dfoprab3s  6397  dfoprab3  6398  dfoprab4  6399  opabn1stprc  6402  mapsncnv  6943  xpcomco  7090  dmaddpq  7710  dmmulpq  7711  recmulnqg  7722  enq0enq  7762  ltrelxr  8350  ltxr  10127  shftidt2  11542  releqgg  13973  eqgex  13974  prdsex  14114  prdsval  14115  prdsbaslemss  14116  dvdsrzring  14877  lmfval  15184  lmbr  15204  cnmptid  15272  lgsquadlem3  16078  wksfval  16443