Theorem riotaeqbidv 6614

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)

Hypotheses

Ref	Expression
riotaeqbidv.1	|- ( ph -> A = B )
riotaeqbidv.2	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
riotaeqbidv	|- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)   B( x)

Proof of Theorem riotaeqbidv

Step	Hyp	Ref	Expression
1		riotaeqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	riotabidv 6613	. 2 |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )
3		riotaeqbidv.1	. . 3 |- ( ph -> A = B )
4	3	riotaeqdv 6612	. 2 |- ( ph -> ( iota_ x e. A ch ) = ( iota_ x e. B ch ) )
5	2, 4	eqtrd 2656	1 |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   iota_crio 6610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-iota 5851  df-riota 6611

This theorem is referenced by:  dfoi  8416  oieq1  8417  oieq2  8418  ordtypecbv  8422  ordtypelem3  8425  zorn2lem1  9318  zorn2g  9325  cidfval  16337  cidval  16338  cidpropd  16370  lubfval  16978  glbfval  16991  grpinvfval  17460  pj1fval  18107  mpfrcl  19518  evlsval  19519  q1pval  23913  ig1pval  23932  mirval  25550  midf  25668  ismidb  25670  lmif  25677  islmib  25679  gidval  27366  grpoinvfval  27376  pjhfval  28255  cvmliftlem5  31271  cvmliftlem15  31280  scutval  31911  trlfset  35447  dicffval  36463  dicfval  36464  dihffval  36519  dihfval  36520  hvmapffval  37047  hvmapfval  37048  hdmap1fval  37086  hdmapffval  37118  hdmapfval  37119  hgmapfval  37178  wessf1ornlem  39371