![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brralrspcev | Structured version Visualization version GIF version |
Description: Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
Ref | Expression |
---|---|
brralrspcev | ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 5151 | . . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) | |
2 | 1 | ralbidv 3178 | . 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵)) |
3 | 2 | rspcev 3612 | 1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 class class class wbr 5147 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 |
This theorem is referenced by: axpre-sup 11160 fimaxre2 12155 supaddc 12177 supadd 12178 supmul1 12179 supmullem2 12181 supmul 12182 rpnnen1lem2 12957 iccsupr 13415 supicc 13474 supiccub 13475 supicclub 13476 flval3 13776 fsequb 13936 01sqrexlem3 15187 caubnd2 15300 caubnd 15301 lo1bdd2 15464 lo1bddrp 15465 climcnds 15793 ruclem12 16180 maxprmfct 16642 prmreclem1 16845 prmreclem6 16850 ramz 16954 pgpssslw 19475 gexex 19713 icccmplem2 24321 icccmplem3 24322 reconnlem2 24325 cnllycmp 24454 cncmet 24821 ivthlem2 24951 ivthlem3 24952 cniccbdd 24960 ovolunlem1 24996 ovoliunlem1 25001 ovoliun2 25005 ioombl1lem4 25060 uniioombllem2 25082 uniioombllem6 25087 mbfinf 25164 mbflimsup 25165 itg1climres 25214 itg2i1fseq 25255 itg2i1fseq2 25256 itg2cnlem1 25261 plyeq0lem 25706 ulmbdd 25892 mtestbdd 25899 iblulm 25901 emcllem6 26485 lgambdd 26521 ftalem3 26559 ubthlem2 30102 ubthlem3 30103 htthlem 30148 rge0scvg 32867 esumpcvgval 33014 oddpwdc 33291 mblfinlem3 36465 ismblfin 36467 itg2addnc 36480 ubelsupr 43637 rexabslelem 44063 limsupubuz 44364 liminfreuzlem 44453 dvdivbd 44574 sge0supre 45040 sge0rnbnd 45044 meaiuninc2 45133 hoidmvlelem1 45246 hoidmvlelem4 45249 smfinflem 45468 |
Copyright terms: Public domain | W3C validator |