Theorem opabbii 5179

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

Syntax hints:   ↔ wb 209   = wceq 1567  {copab 5174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-opab 5175

This theorem is referenced by:  mptv  5218  2rbropap  5547  dfid4  5555  fconstmpt  5721  xpundi  5728  xpundir  5729  cnvi  5869  csbcnv  5870  csbcnvOLD  5871  cnvco  5873  resopab  6034  opabresid  6050  cnvun  6137  cnvxp  6153  cnvcnv3  6185  coundi  6245  coundir  6246  mptun  6679  fvopab6  7022  fmptsng  7164  fmptsnd  7165  cbvoprab1  7495  cbvoprab12  7497  dmoprabss  7512  mpomptx  7521  resoprab  7526  elrnmpores  7546  ov6g  7572  1st2val  8010  2nd2val  8011  dfoprab3s  8046  dfoprab3  8047  dfoprab4  8048  opabn1stprc  8051  mptmpoopabbrd  8074  fsplit  8108  mapsncnv  8887  xpcomco  9051  marypha2lem2  9392  oemapso  9647  ttrclresv  9682  leweon  9991  r0weon  9992  compsscnv  10351  fpwwe  10627  ltrelxr  11266  ltxrlt  11276  ltxr  13136  shftidt2  15114  prdsle  17511  prdsless  17512  prdsleval  17526  dfiso2  17825  joindm  18425  meetdm  18439  gaorb  19373  efgcpbllema  19820  frgpuplem  19838  dvdsrzring  21576  pjfval2  21824  ltbval  22159  ltbwe  22160  opsrle  22163  opsrtoslem1  22171  opsrtoslem2  22172  lmfval  23354  lmbr  23380  lgsquadlem3  27508  perpln1  28945  outpasch  28992  ishpg  28996  axcontlem2  29252  wksfval  29896  wlkson  29941  pthsfval  30005  ispth  30007  dfadj2  32174  dmadjss  32176  cnvadj  32181  mpomptxf  32960  lsmsnorb2  33645  satfv0  35745  satfvsuclem1  35746  satfvsuclem2  35747  satfbrsuc  35753  satf0  35759  satf0suclem  35762  fmlasuc0  35771  dfsuccf2  36328  fneer  36749  bj-dfmpoa  37643  bj-mpomptALT  37644  bj-brab2a1  37676  bj-imdiridlem  37712  bj-opabco  37715  opropabco  38258  xpv  38796  cnvepres  38838  inxp2  38909  disjecxrn  38946  xrninxp  38949  xrninxp2  38950  rnxrnres  38956  rnxrncnvepres  38957  rnxrnidres  38958  blockadjliftmap  38992  dfsucmap3  38997  dfsucmap4  38999  dfcoss2  39037  dfcoss3  39038  cosscnv  39040  coss1cnvres  39041  coss2cnvepres  39042  1cossres  39053  dfcoels  39054  ressn2  39066  br1cosscnvxrn  39098  1cosscnvxrn  39099  coss0  39103  cossid  39104  dfssr2  39113  dfpetparts2  39506  dfpeters2  39508  petseq  39510  cmtfvalN  39869  cmtvalN  39870  cvrfval  39927  cvrval  39928  dicval2  41838  aks6d1c1p1rcl  42760  aks6d1c1rh  42777  fgraphopab  43815  fgraphxp  43816  modelaxreplem2  45573  mptssid  45841  dfnelbr2  47892  opabbrfex0d  47905  opabbrfexd  47907  upwlksfval  48782  xpsnopab  48804  mpomptx2  48993  upfval2  49833