Theorem opabbii 4161

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 4160	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

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

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-opab 4156

This theorem is referenced by:  mptv  4191  fconstmpt  4779  xpundi  4788  xpundir  4789  inxp  4870  cnvco  4921  resopab  5063  opabresid  5072  cnvi  5148  cnvun  5149  cnvin  5151  cnvxp  5162  cnvcnv3  5193  coundi  5245  coundir  5246  mptun  5471  fvopab6  5752  cbvoprab1  6103  cbvoprab12  6105  dmoprabss  6113  mpomptx  6122  resoprab  6127  ov6g  6170  dfoprab3s  6362  dfoprab3  6363  dfoprab4  6364  opabn1stprc  6367  mapsncnv  6907  xpcomco  7053  dmaddpq  7642  dmmulpq  7643  recmulnqg  7654  enq0enq  7694  ltrelxr  8282  ltxr  10054  shftidt2  11455  prdsex  13415  prdsval  13419  prdsbaslemss  13420  releqgg  13870  eqgex  13871  dvdsrzring  14682  lmfval  14987  lmbr  15007  cnmptid  15075  lgsquadlem3  15881  wksfval  16246