Theorem cbvriotav 6894

Description: Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)

Hypothesis

Ref	Expression
cbvriotav.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvriotav	⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvriotav

Step	Hyp	Ref	Expression
1		nfv 1957	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1957	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvriotav.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvriota 6893	1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  ℩crio 6882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-rex 3096  df-sn 4399  df-uni 4672  df-iota 6099  df-riota 6883

This theorem is referenced by:  ordtypecbv  8711  fin23lem27  9485  zorn2g  9660  uspgredg2v  26570  usgredg2v  26573  cnlnadji  29507  nmopadjlei  29519  cvmliftlem15  31879  cvmliftiota  31882  cvmlift2  31897  cvmlift3lem7  31906  cvmlift3  31909  lshpkrlem3  35268  cdleme40v  36625  lcfl7N  37657  lcf1o  37707  lcfrlem39  37737  hdmap1cbv  37958  wessf1ornlem  40298  fourierdlem103  41357  fourierdlem104  41358