# Metamath Proof Explorer

## Theorem rabsubmgmd

Description: Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypotheses rabsubmgmd.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
rabsubmgmd.p
rabsubmgmd.m ${⊢}{\phi }\to {M}\in \mathrm{Mgm}$
rabsubmgmd.cp ${⊢}\left({\phi }\wedge \left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({\theta }\wedge {\tau }\right)\right)\right)\to {\eta }$
rabsubmgmd.th ${⊢}{z}={x}\to \left({\psi }↔{\theta }\right)$
rabsubmgmd.ta ${⊢}{z}={y}\to \left({\psi }↔{\tau }\right)$
rabsubmgmd.et
Assertion rabsubmgmd ${⊢}{\phi }\to \left\{{z}\in {B}|{\psi }\right\}\in \mathrm{SubMgm}\left({M}\right)$

### Proof

Step Hyp Ref Expression
1 rabsubmgmd.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 rabsubmgmd.p
3 rabsubmgmd.m ${⊢}{\phi }\to {M}\in \mathrm{Mgm}$
4 rabsubmgmd.cp ${⊢}\left({\phi }\wedge \left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({\theta }\wedge {\tau }\right)\right)\right)\to {\eta }$
5 rabsubmgmd.th ${⊢}{z}={x}\to \left({\psi }↔{\theta }\right)$
6 rabsubmgmd.ta ${⊢}{z}={y}\to \left({\psi }↔{\tau }\right)$
7 rabsubmgmd.et
8 ssrab2 ${⊢}\left\{{z}\in {B}|{\psi }\right\}\subseteq {B}$
9 8 a1i ${⊢}{\phi }\to \left\{{z}\in {B}|{\psi }\right\}\subseteq {B}$
10 5 elrab ${⊢}{x}\in \left\{{z}\in {B}|{\psi }\right\}↔\left({x}\in {B}\wedge {\theta }\right)$
11 6 elrab ${⊢}{y}\in \left\{{z}\in {B}|{\psi }\right\}↔\left({y}\in {B}\wedge {\tau }\right)$
12 10 11 anbi12i ${⊢}\left({x}\in \left\{{z}\in {B}|{\psi }\right\}\wedge {y}\in \left\{{z}\in {B}|{\psi }\right\}\right)↔\left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)$
13 3 adantr ${⊢}\left({\phi }\wedge \left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)\right)\to {M}\in \mathrm{Mgm}$
14 simprll ${⊢}\left({\phi }\wedge \left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)\right)\to {x}\in {B}$
15 simprrl ${⊢}\left({\phi }\wedge \left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)\right)\to {y}\in {B}$
16 1 2 mgmcl
17 13 14 15 16 syl3anc
18 simpl ${⊢}\left({x}\in {B}\wedge {\theta }\right)\to {x}\in {B}$
19 simpl ${⊢}\left({y}\in {B}\wedge {\tau }\right)\to {y}\in {B}$
20 18 19 anim12i ${⊢}\left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)\to \left({x}\in {B}\wedge {y}\in {B}\right)$
21 simpr ${⊢}\left({x}\in {B}\wedge {\theta }\right)\to {\theta }$
22 simpr ${⊢}\left({y}\in {B}\wedge {\tau }\right)\to {\tau }$
23 21 22 anim12i ${⊢}\left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)\to \left({\theta }\wedge {\tau }\right)$
24 20 23 jca ${⊢}\left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)\to \left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({\theta }\wedge {\tau }\right)\right)$
25 24 4 sylan2 ${⊢}\left({\phi }\wedge \left(\left({x}\in {B}\wedge {\theta }\right)\wedge \left({y}\in {B}\wedge {\tau }\right)\right)\right)\to {\eta }$
26 7 17 25 elrabd
27 12 26 sylan2b
28 27 ralrimivva
29 1 2 issubmgm
30 3 29 syl
31 9 28 30 mpbir2and ${⊢}{\phi }\to \left\{{z}\in {B}|{\psi }\right\}\in \mathrm{SubMgm}\left({M}\right)$