Theorem cbvriotav 6522

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 1830	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvriotav.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvriota 6521	1 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ℩crio 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-sn 4126  df-uni 4373  df-iota 5768  df-riota 6511

This theorem is referenced by:  ordtypecbv  8305  fin23lem27  9033  zorn2g  9208  usgraidx2v  25922  cnlnadji  28319  nmopadjlei  28331  cvmliftlem15  30534  cvmliftiota  30537  cvmlift2  30552  cvmlift3lem7  30561  cvmlift3  30564  lshpkrlem3  33417  cdleme40v  34775  lcfl7N  35808  lcf1o  35858  lcfrlem39  35888  hdmap1cbv  36110  wessf1ornlem  38366  fourierdlem103  39102  fourierdlem104  39103  uspgredg2v  40451  usgredg2v  40454