Theorem opabbii 4156

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

Syntax hints:   ↔ wb 105   = wceq 1397  {copab 4149

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-opab 4151

This theorem is referenced by:  mptv  4186  fconstmpt  4773  xpundi  4782  xpundir  4783  inxp  4864  cnvco  4915  resopab  5057  opabresid  5066  cnvi  5141  cnvun  5142  cnvin  5144  cnvxp  5155  cnvcnv3  5186  coundi  5238  coundir  5239  mptun  5464  fvopab6  5743  cbvoprab1  6092  cbvoprab12  6094  dmoprabss  6102  mpomptx  6111  resoprab  6116  ov6g  6159  dfoprab3s  6352  dfoprab3  6353  dfoprab4  6354  opabn1stprc  6357  mapsncnv  6863  xpcomco  7009  dmaddpq  7598  dmmulpq  7599  recmulnqg  7610  enq0enq  7650  ltrelxr  8239  ltxr  10009  shftidt2  11392  prdsex  13351  prdsval  13355  prdsbaslemss  13356  releqgg  13806  eqgex  13807  dvdsrzring  14616  lmfval  14916  lmbr  14936  cnmptid  15004  lgsquadlem3  15807  wksfval  16172