Theorem brralrspcev 5090

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 5034	. . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵))
2	1	ralbidv 3162	. 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵))
3	2	rspcev 3571	1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  axpre-sup  10580  fimaxre2  11574  supaddc  11595  supadd  11596  supmul1  11597  supmullem2  11599  supmul  11600  rpnnen1lem2  12364  iccsupr  12820  supicc  12879  supiccub  12880  supicclub  12881  flval3  13180  fsequb  13338  sqrlem3  14596  caubnd2  14709  caubnd  14710  lo1bdd2  14873  lo1bddrp  14874  climcnds  15198  ruclem12  15586  maxprmfct  16043  prmreclem1  16242  prmreclem6  16247  ramz  16351  pgpssslw  18731  gexex  18966  icccmplem2  23428  icccmplem3  23429  reconnlem2  23432  cnllycmp  23561  cncmet  23926  ivthlem2  24056  ivthlem3  24057  cniccbdd  24065  ovolunlem1  24101  ovoliunlem1  24106  ovoliun2  24110  ioombl1lem4  24165  uniioombllem2  24187  uniioombllem6  24192  mbfinf  24269  mbflimsup  24270  itg1climres  24318  itg2i1fseq  24359  itg2i1fseq2  24360  itg2cnlem1  24365  plyeq0lem  24807  ulmbdd  24993  mtestbdd  25000  iblulm  25002  emcllem6  25586  lgambdd  25622  ftalem3  25660  ubthlem2  28654  ubthlem3  28655  htthlem  28700  rge0scvg  31302  esumpcvgval  31447  oddpwdc  31722  mblfinlem3  35096  ismblfin  35098  itg2addnc  35111  ubelsupr  41649  rexabslelem  42055  limsupubuz  42355  liminfreuzlem  42444  dvdivbd  42565  sge0supre  43028  sge0rnbnd  43032  meaiuninc2  43121  hoidmvlelem1  43234  hoidmvlelem4  43237  smfinflem  43448