Theorem opabbii 4193

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

Syntax hints:   ↔ wb 105   = wceq 1402  {copab 4186

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-opab 4188

This theorem is referenced by:  mptv  4223  fconstmpt  4817  xpundi  4826  xpundir  4827  inxp  4909  cnvco  4960  resopab  5102  opabresid  5111  cnvi  5187  cnvun  5188  cnvin  5190  cnvxp  5201  cnvcnv3  5232  coundi  5284  coundir  5285  mptun  5510  fvopab6  5796  cbvoprab1  6150  cbvoprab12  6152  dmoprabss  6160  mpomptx  6169  resoprab  6174  ov6g  6217  dfoprab3s  6414  dfoprab3  6415  dfoprab4  6416  opabn1stprc  6419  mapsncnv  6967  xpcomco  7114  dmaddpq  7736  dmmulpq  7737  recmulnqg  7748  enq0enq  7788  ltrelxr  8376  ltxr  10156  shftidt2  11575  releqgg  14000  eqgex  14001  prdsex  14149  prdsval  14150  prdsbaslemss  14151  dvdsrzring  14910  lmfval  15217  lmbr  15237  cnmptid  15305  lgsquadlem3  16112  wksfval  16477