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  4721  xpundi  4730  xpundir  4731  inxp  4811  cnvco  4862  resopab  5002  opabresid  5011  cnvi  5086  cnvun  5087  cnvin  5089  cnvxp  5100  cnvcnv3  5131  coundi  5183  coundir  5184  mptun  5406  fvopab6  5675  cbvoprab1  6016  cbvoprab12  6018  dmoprabss  6026  mpomptx  6035  resoprab  6040  ov6g  6083  dfoprab3s  6275  dfoprab3  6276  dfoprab4  6277  mapsncnv  6781  xpcomco  6920  dmaddpq  7491  dmmulpq  7492  recmulnqg  7503  enq0enq  7543  ltrelxr  8132  ltxr  9896  shftidt2  11085  prdsex  13043  prdsval  13047  prdsbaslemss  13048  releqgg  13498  eqgex  13499  dvdsrzring  14307  lmfval  14606  lmbr  14627  cnmptid  14695  lgsquadlem3  15498