Theorem opabbii 4154

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

Syntax hints:   ↔ wb 105   = wceq 1395  {copab 4147

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-opab 4149

This theorem is referenced by:  mptv  4184  fconstmpt  4771  xpundi  4780  xpundir  4781  inxp  4862  cnvco  4913  resopab  5055  opabresid  5064  cnvi  5139  cnvun  5140  cnvin  5142  cnvxp  5153  cnvcnv3  5184  coundi  5236  coundir  5237  mptun  5461  fvopab6  5739  cbvoprab1  6088  cbvoprab12  6090  dmoprabss  6098  mpomptx  6107  resoprab  6112  ov6g  6155  dfoprab3s  6348  dfoprab3  6349  dfoprab4  6350  opabn1stprc  6353  mapsncnv  6859  xpcomco  7005  dmaddpq  7589  dmmulpq  7590  recmulnqg  7601  enq0enq  7641  ltrelxr  8230  ltxr  10000  shftidt2  11383  prdsex  13342  prdsval  13346  prdsbaslemss  13347  releqgg  13797  eqgex  13798  dvdsrzring  14607  lmfval  14907  lmbr  14927  cnmptid  14995  lgsquadlem3  15798  wksfval  16119