Theorem brralrspcev 5209

Description: Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)

Assertion

Ref	Expression
brralrspcev	⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅   𝑥,𝑋   𝑥,𝑌

Allowed substitution hints:   𝐴(𝑦)   𝑅(𝑦)   𝑋(𝑦)   𝑌(𝑦)

Proof of Theorem brralrspcev

Step	Hyp	Ref	Expression
1		breq2 5153	. . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵))
2	1	ralbidv 3167	. 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵))
3	2	rspcev 3606	1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3050  ∃wrex 3059   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150

This theorem is referenced by:  axpre-sup  11193  fimaxre2  12190  supaddc  12212  supadd  12213  supmul1  12214  supmullem2  12216  supmul  12217  rpnnen1lem2  12992  iccsupr  13452  supicc  13511  supiccub  13512  supicclub  13513  flval3  13814  fsequb  13974  01sqrexlem3  15225  caubnd2  15338  caubnd  15339  lo1bdd2  15502  lo1bddrp  15503  climcnds  15831  ruclem12  16219  maxprmfct  16681  prmreclem1  16886  prmreclem6  16891  ramz  16995  pgpssslw  19578  gexex  19817  icccmplem2  24779  icccmplem3  24780  reconnlem2  24783  cnllycmp  24922  cncmet  25290  ivthlem2  25421  ivthlem3  25422  cniccbdd  25430  ovolunlem1  25466  ovoliunlem1  25471  ovoliun2  25475  ioombl1lem4  25530  uniioombllem2  25552  uniioombllem6  25557  mbfinf  25634  mbflimsup  25635  itg1climres  25684  itg2i1fseq  25725  itg2i1fseq2  25726  itg2cnlem1  25731  plyeq0lem  26184  ulmbdd  26374  mtestbdd  26381  iblulm  26383  emcllem6  26973  lgambdd  27009  ftalem3  27047  ubthlem2  30747  ubthlem3  30748  htthlem  30793  rge0scvg  33662  esumpcvgval  33809  oddpwdc  34086  mblfinlem3  37244  ismblfin  37246  itg2addnc  37259  ubelsupr  44491  rexabslelem  44905  limsupubuz  45206  liminfreuzlem  45295  dvdivbd  45416  sge0supre  45882  sge0rnbnd  45886  meaiuninc2  45975  hoidmvlelem1  46088  hoidmvlelem4  46091  smfinflem  46310

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »