Theorem opabbii 4101

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

Syntax hints:   ↔ wb 105   = wceq 1364  {copab 4094

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-opab 4096

This theorem is referenced by:  mptv  4131  fconstmpt  4711  xpundi  4720  xpundir  4721  inxp  4801  cnvco  4852  resopab  4991  opabresid  5000  cnvi  5075  cnvun  5076  cnvin  5078  cnvxp  5089  cnvcnv3  5120  coundi  5172  coundir  5173  mptun  5392  fvopab6  5661  cbvoprab1  5998  cbvoprab12  6000  dmoprabss  6008  mpomptx  6017  resoprab  6022  ov6g  6065  dfoprab3s  6257  dfoprab3  6258  dfoprab4  6259  mapsncnv  6763  xpcomco  6894  dmaddpq  7465  dmmulpq  7466  recmulnqg  7477  enq0enq  7517  ltrelxr  8106  ltxr  9869  shftidt2  11016  prdsex  12973  prdsval  12977  prdsbaslemss  12978  releqgg  13428  eqgex  13429  dvdsrzring  14237  lmfval  14536  lmbr  14557  cnmptid  14625  lgsquadlem3  15428